Rename runtime to leaf in samples

momvart · tkhang1999 · commit 9f081231a437 · 2024-01-29T16:08:12.000-08:00
diff --git a/README.md b/README.md
@@ -167,7 +167,7 @@ $ cargo run -- --emit=mir main.rs
 ### Example reasoning
 - Let's look at the example located at `leaf/samples/function/sym_arg/main.rs`.
 ```rust
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = 10.mark_symbolic();
diff --git a/samples/TheAlgorithms/ciphers/base64.rs b/samples/TheAlgorithms/ciphers/base64.rs
@@ -232,7 +232,7 @@ mod tests {
     }
 
     pub(super) fn encode_symbolic() {
-        use runtime::annotations::Symbolizable;
+        use leaf::annotations::Symbolizable;
 
         let data = b"\xd31\xc9\x87D\xfe\xaa\xb3\xff\xef\x8c\x0eoD";
         let mut data_sym = NSByteString::new();
@@ -248,7 +248,7 @@ mod tests {
     }
 
     pub(super) fn decode_symbolic() {
-        use runtime::annotations::Symbolizable;
+        use leaf::annotations::Symbolizable;
 
         let encoded = b"0zHJh0T+qrP/74wOb0Q=";
         let mut encoded_sym = NSByteString::new();
@@ -264,7 +264,7 @@ mod tests {
     }
 
     pub(super) fn encode_decode_symbolic() {
-        use runtime::annotations::Symbolizable;
+        use leaf::annotations::Symbolizable;
 
         let data = b"Lorem Ipsum";
         let mut data_sym = NSByteString::new();
diff --git a/samples/TheAlgorithms/sorting/quick_sort.rs b/samples/TheAlgorithms/sorting/quick_sort.rs
@@ -1,6 +1,6 @@
 /* Adapted from: https://github.com/TheAlgorithms/Rust */
 
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     all_symbolic();
diff --git a/samples/assignment/addr_of/comapre_with_sym.rs b/samples/assignment/addr_of/comapre_with_sym.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let a = 20;
diff --git a/samples/assignment/bin_op/checked_ops/checked_add.rs b/samples/assignment/bin_op/checked_ops/checked_add.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let mut x = 20_u64.mark_symbolic();
diff --git a/samples/assignment/bin_op/checked_ops/checked_mul.rs b/samples/assignment/bin_op/checked_ops/checked_mul.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let mut x = 20_u32.mark_symbolic();
diff --git a/samples/assignment/bin_op/checked_ops/checked_sub.rs b/samples/assignment/bin_op/checked_ops/checked_sub.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let mut x = 20_u16.mark_symbolic();
diff --git a/samples/assignment/bin_op/checked_ops/unsigned_test.rs b/samples/assignment/bin_op/checked_ops/unsigned_test.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let mut x = 0_u64.mark_symbolic();
diff --git a/samples/assignment/bin_op/shift/differing_types.rs b/samples/assignment/bin_op/shift/differing_types.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let a1 = 0b1u8.mark_symbolic() << 7u8; // == 2^15
diff --git a/samples/basic/is_sorted/main.rs b/samples/basic/is_sorted/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let arr = get_symbolic_array();
diff --git a/samples/basic/sudoku_checker/main.rs b/samples/basic/sudoku_checker/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let board = get_symbolic_board();
diff --git a/samples/branching/assert/boundscheck.rs b/samples/branching/assert/boundscheck.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let ar = [1, 2];
diff --git a/samples/branching/assert/divbyzero.rs b/samples/branching/assert/divbyzero.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let mut x = 20_u16.mark_symbolic();
diff --git a/samples/branching/assert/overflow.rs b/samples/branching/assert/overflow.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let mut x: u64 = 10.mark_symbolic();
diff --git a/samples/branching/assert/overflow_neg.rs b/samples/branching/assert/overflow_neg.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let mut x: i32 = 10.mark_symbolic();
diff --git a/samples/branching/assert/rembyzero.rs b/samples/branching/assert/rembyzero.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let mut x = 20_u16.mark_symbolic();
diff --git a/samples/branching/if_basic/main.rs b/samples/branching/if_basic/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = get_num().mark_symbolic();
diff --git a/samples/branching/if_let/main.rs b/samples/branching/if_let/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = 10_u8.mark_symbolic();
diff --git a/samples/casting/dyn_star/symbolic.rs b/samples/casting/dyn_star/symbolic.rs
@@ -1,6 +1,6 @@
 #![feature(dyn_star)]
 
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 trait Bar {
     fn bar(&self) -> usize;
diff --git a/samples/casting/dyn_star/symbolic_inner.rs b/samples/casting/dyn_star/symbolic_inner.rs
@@ -1,6 +1,6 @@
 #![feature(dyn_star)]
 
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 trait Bar {
     fn bar(&self) -> usize;
diff --git a/samples/casting/numeric/int_only/sym_main.rs b/samples/casting/numeric/int_only/sym_main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 #[allow(unused_variables)]
 
diff --git a/samples/casting/pointer/expose/sym_ptr_to_usize.rs b/samples/casting/pointer/expose/sym_ptr_to_usize.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = 1.mark_symbolic();
diff --git a/samples/crates/sym_basic_bin/src/main.rs b/samples/crates/sym_basic_bin/src/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 mod child;
 
diff --git a/samples/function/closures/sym_basic.rs b/samples/function/closures/sym_basic.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = 10.mark_symbolic();
diff --git a/samples/function/closures/sym_capturing.rs b/samples/function/closures/sym_capturing.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = 10.mark_symbolic();
diff --git a/samples/function/sym_arg/main.rs b/samples/function/sym_arg/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = 10.mark_symbolic();
diff --git a/samples/function/sym_arg_ret/main.rs b/samples/function/sym_arg_ret/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = 10.mark_symbolic();
diff --git a/samples/function/sym_inner/main.rs b/samples/function/sym_inner/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = (-4).mark_symbolic();
diff --git a/samples/function/sym_recursive/main.rs b/samples/function/sym_recursive/main.rs
@@ -2,7 +2,7 @@
  * Ideally in a way that can be directly solved by the solver.
  */
 
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = (-4).mark_symbolic();
diff --git a/samples/function/sym_ret/main.rs b/samples/function/sym_ret/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = read();
diff --git a/samples/misc/constant_folding/main.rs b/samples/misc/constant_folding/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = 0_u8.mark_symbolic();
diff --git a/samples/misc/multiple_vars/main.rs b/samples/misc/multiple_vars/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = 10.mark_symbolic();
diff --git a/samples/misc/sym_field/main.rs b/samples/misc/sym_field/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let foo = Foo {
diff --git a/samples/projection/downcast/enum/main.rs b/samples/projection/downcast/enum/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let a = Bar::First(1, 2.mark_symbolic());
diff --git a/samples/projection/downcast/transmute/symbolic_det.rs b/samples/projection/downcast/transmute/symbolic_det.rs
@@ -1,6 +1,6 @@
 use std::mem::transmute;
 
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = 10u32.mark_symbolic();
diff --git a/samples/projection/field/main.rs b/samples/projection/field/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let a = Bar {
diff --git a/samples/projection/index/main.rs b/samples/projection/index/main.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let a = [1, 2, 3.mark_symbolic()];
diff --git a/samples/sym_place/read/addr_of.rs b/samples/sym_place/read/addr_of.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let array = [1, 2, 3, 4];
diff --git a/samples/sym_place/read/index.rs b/samples/sym_place/read/index.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let array = [1, 2, 3, 4];
diff --git a/samples/sym_place/read/index_from_end.rs b/samples/sym_place/read/index_from_end.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let array: [&[u8]; 2] = [&[1, 2], &[3, 4, 5]];
diff --git a/samples/sym_place/read/index_on_transmute.rs b/samples/sym_place/read/index_on_transmute.rs
@@ -1,6 +1,6 @@
 use std::mem::transmute;
 
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let x = 10u32.mark_symbolic();
diff --git a/samples/sym_place/read/len.rs b/samples/sym_place/read/len.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let array: [&[u8]; 2] = [&[1, 2], &[3]];
diff --git a/samples/sym_place/read/long_chain.rs b/samples/sym_place/read/long_chain.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let array = [
diff --git a/samples/sym_place/read/long_chain_noenum.rs b/samples/sym_place/read/long_chain_noenum.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let array = [
diff --git a/samples/sym_place/read/multi_dim_index.rs b/samples/sym_place/read/multi_dim_index.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let array = [[1, 2], [3, 4]];
diff --git a/samples/sym_place/read/proj_on_index.rs b/samples/sym_place/read/proj_on_index.rs
@@ -1,4 +1,4 @@
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let array = [Point { x: 1, y: 2 }, Point { x: 3, y: 4 }];
diff --git a/samples/sym_place/read/transmute_on_index.rs b/samples/sym_place/read/transmute_on_index.rs
@@ -1,6 +1,6 @@
 use std::mem::transmute;
 
-use runtime::annotations::Symbolizable;
+use leaf::annotations::Symbolizable;
 
 fn main() {
     let array = [10u32, 11, 12, 13];

Original file line number	Diff line number	Diff line change
`@@ -232,7 +232,7 @@ mod tests {`
`232`	`232`	`}`
`233`	`233`
`234`	`234`	`pub(super) fn encode_symbolic() {`
`235`		`- use runtime::annotations::Symbolizable;`
	`235`	`+ use leaf::annotations::Symbolizable;`
`236`	`236`
`237`	`237`	`let data = b"\xd31\xc9\x87D\xfe\xaa\xb3\xff\xef\x8c\x0eoD";`
`238`	`238`	`let mut data_sym = NSByteString::new();`
`@@ -248,7 +248,7 @@ mod tests {`
`248`	`248`	`}`
`249`	`249`
`250`	`250`	`pub(super) fn decode_symbolic() {`
`251`		`- use runtime::annotations::Symbolizable;`
	`251`	`+ use leaf::annotations::Symbolizable;`
`252`	`252`
`253`	`253`	`let encoded = b"0zHJh0T+qrP/74wOb0Q=";`
`254`	`254`	`let mut encoded_sym = NSByteString::new();`
`@@ -264,7 +264,7 @@ mod tests {`
`264`	`264`	`}`
`265`	`265`
`266`	`266`	`pub(super) fn encode_decode_symbolic() {`
`267`		`- use runtime::annotations::Symbolizable;`
	`267`	`+ use leaf::annotations::Symbolizable;`
`268`	`268`
`269`	`269`	`let data = b"Lorem Ipsum";`
`270`	`270`	`let mut data_sym = NSByteString::new();`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-use runtime::annotations::Symbolizable;`
	`1`	`+use leaf::annotations::Symbolizable;`
`2`	`2`
`3`	`3`	`fn main() {`
`4`	`4`	`let a = 20;`