Add more and better Rust examples

src/example-archive/Rust/broken/error-crash/00008-pointer-compare.c

@@ -0,0 +1,52 @@
+// Tags: main, pointers
+/** Description: 
+
+    This example corrects the broken 03-lifetimes-broken.c. Here `r`
+    is inside the scope of `x` so things work out. However the
+    lifetime usage is not very interesting.
+
+*/
+
+/* Rust code:
+
+fn main() {
+    let x = 42; // 'x' lives throughout the outer scope
+    let r = borrow(&x); // 'r' now correctly borrows 'x' and can be used as long as 'x' is alive
+    println!("The number is: {}", r); // Safe to use 'r' here
+}
+
+fn borrow<'a>(input: &'a i32) -> &'a i32 {
+    input
+}
+
+*/
+
+/* C + CN translation */
+
+
+//#include <stdio.h>
+// Function to "borrow" an integer pointer
+int* compare(int* p, int* bound)
+  /*@ requires take vp0 = Block<int>(p);
+               take vb0 = Block<int>(bound);
+      ensures take vp1 = Block<int>(p);
+              take vb1 = Block<int>(bound);
+	      return == p;
+  @*/
+{
+  if (p==bound){
+    //printf("yes");
+    // Do something
+  }
+  return p;  // Return the input pointer
+}
+
+int main() {
+  int x[] = {42, 0};  // 'x' lives throughout the outer scope
+  int* r = compare(x, x+1);  // 'r' now correctly points to 'x' and can be used as long as 'x' is alive
+  int ret = *r; // Safe to use 'r' here, as 'x' is still in scope
+
+
+  //printf("%d", ret);
+  return ret; 
+}

src/example-archive/Rust/broken/error-crash/00012-move.c

@@ -0,0 +1,79 @@
+// Tags: Rust, strings
+
+// Tags: main, pointers
+/** Description: 
+
+    Rust's ownership system is governed by three main rules:
+
+    1. Each value in Rust has an owner.
+    2. There can only be one owner at a time.
+    3. When the owner goes out of scope, the value will be dropped.
+
+    In Rust, the code below would fail to typecheck because the
+    assignment from `s1` to `s2` transfers the ownership of the
+    pointer from `s1` to `s2`. Consequently, `s1` becomes unusable
+    while `s2` is in scope.
+
+
+    In contrast, CN treats ownership not as an attribute of an entity,
+    but as a transient aspect of the program's execution—a 'ghost
+    state' that does not impact performance. As a result, there are no
+    ownership transfers in CN, allowing verification of the example
+    without issues.
+
+
+    Note that in Rust, `use_string` accepts a slice, which is
+    essentially a 'fat pointer' comprising a pointer, a length, and a
+    capacity. To achieve a similar functionality in C, we must
+    explicitly pass the length `len` as an argument. More details
+    about slices can be found in `slices.c`."
+
+*/
+
+/* Rust code:
+
+fn move(){
+  let x = 42;
+  let s1 = &x;
+  let s2 = s1;
+  use_string(s1);
+}
+*/
+
+
+// Allocates and populates a string of size `len`. 
+extern char *createString (unsigned int len);
+/*@ spec createString(pointer p, u32 len);
+    requires true;
+    ensures  take vp1 = each(u32 i; i < len) { Owned<char>( array_shift<char>(return, i)) };
+@*/
+
+extern char *freeString (char* p, unsigned int len);
+/*@ spec freeString(pointer p, u32 len);
+    requires take vp1 = each(u32 i; i < len) { Owned<char>( array_shift<char>(p, i)) };
+    ensures true;
+@*/
+
+// Uses a string, e.g. IO
+extern void use_string(char* p, unsigned int len);
+/*@ spec use_string(pointer p, u32 len);
+    requires take vp0 = each(u32 i; i < len) { Owned<char>( array_shift<char>(p, i)) };
+    ensures  take vp1 = each(u32 i; i < len) { Owned<char>( array_shift<char>(p, i)) };
+@*/
+
+void move()
+{
+  unsigned int len = 13;
+  char* s1 = createString(len);
+  char* s2 = s1;
+
+  use_string(s1, len); // Without move, we can still use `s1`
+  use_string(s2, len); // We can call use_string again on `s2`, as long as its
+	               // spec returns the ownership.
+
+  freeString(s2, len);
+}
+
+int main(){
+  move();
+}

src/example-archive/Rust/broken/error-crash/00013-slices.c

@@ -0,0 +1,87 @@
+// Tags: Rust, strings
+
+// Tags: main, pointers
+/** Description: 
+
+    Rust Slices provide a safe view into an array and manage both
+    bounds and borrowing rules automatically. This system prevents
+    common runtime errors such as buffer overflows and illegal memory
+    access. Rust's borrow checker enforces access rules that ensure
+    the data is neither modified unexpectedly nor accessed beyond its
+    life, thus maintaining safety across the function's execution.
+
+    On the other hand, the CN uses iterated resources to reason about
+    array ownershiop.  For example, the precondition for `has_zero` require that
+
+    `take vp0 = each(u32 i; i < len) { Owned<int>( array_shift<int>(p, i)) };`
+
+    This iterated resource corresponds to Rust's slices and states
+    that all the elements, from index 0 to `len`, are owned.
+
+    Often times resources have to be manually extracted from an
+    iterated resource by using the `extract` hint. In the example,
+    this is used before accessing `p[i]` to demonstrate that the
+    execution has the ownership required to read the value.
+
+*/
+
+/* Rust code:
+
+fn has_zero(p: &[i32]) -> bool {
+    // Iterate over the slice and check if any element is zero
+    for &item in p {
+        if item == 0 {  // Check for zero instead of space (correcting the apparent mistake in the original C code)
+            return true;
+        }
+    }
+    false
+}
+
+fn use_slices() -> bool {
+    let fibs: [i32; 10] = [1, 1, 2, 3, 5, 8, 13, 0, 21, 34];
+    let s1 = has_zero(&fibs);  // Pass a slice of the array
+
+    s1
+}
+
+fn main() {
+    let ret_ = use_slices();
+    println!("Contains zero: {}", ret_);
+}
+
+ */
+
+#include <stdbool.h> // Include for `bool` type
+
+
+// Check if there is a space within the first `len` characters of the string `s`
+bool has_zero(const int *p, unsigned int len)
+/*@ requires take vp0 = each(u32 i; i < len) { Owned<int>( array_shift<int>(p, i)) };
+    ensures  take vp2 = each(u32 i; i < len) { Owned<int>( array_shift<int>(p, i)) };
+@*/
+{
+    for (unsigned int i = 0; i < len; i++)
+      /*@ inv take vp1 = each(u32 j; j < len) { Owned<int>( array_shift<int>(p, j)) };
+	  {p} unchanged;
+      @*/
+      {
+	/*@ extract Owned<unsigned int>, i; @*/
+        if (p[i] == 0) {
+            return true; // Return true if a space is found
+        }
+    }
+    return false; // Return false if no space is found
+}
+
+
+bool use_slices()
+{
+  int fibs[10] = {1,1,2,3,5,8,13,0,21,34};
+  bool s1 = has_zero(fibs,10); // `s1_` is unused
+
+  return s1;
+}
+
+int main(){
+  bool ret_ = use_slices();
+}

src/example-archive/Rust/broken/error-crash/00014-exception.c

@@ -0,0 +1,16 @@
+// Tags: arrays
+
+// Tags: main, pointers
+/** Description: 
+
+Exception triggered by a spec creating arrays.
+
+*/
+
+
+// Allocates and populates an array of size `len`. 
+extern int *createArray (unsigned int len);
+/*@ spec createArray(pointer p, u32 len);
+    requires true;
+    ensures  take vp1 = each(u32 i; i < len) { Owned<int>( array_shift<int>(return, i)) };
+@*/

src/example-archive/Rust/working/00009-read_write.c

@@ -0,0 +1,78 @@
+// Tags: Rust, strings, main, custom malloc
+
+// Tags: main, pointers
+/** Description: 
+
+    CN and Rust have different mutability models. This example
+    highlights one particular difference:
+
+    In Rust there are mutable (i.e. read-write) reference `&mut p`
+    read-only reference `&p`. Safe Rust doens't allow uninitialized
+    memory, so there is no write-only permission.
+
+    In CN `Block<T>(p)` represents uninitialized memory and is
+    write-only. The `Owned<T>(p)` permission is read-write. There is
+    no read-only permission.
+
+    A `Owned<T>(p)` permission is strictly stronger than a
+    `Block<T>(p)` and can always be lowered to satisfy the former.
+    After the write `*s1 = 42;` the resource becomes initialized, so
+    the ownership is increased to `Owned<T>(p)`, but the stronger
+    permission is enough to satisfy the the spec of `freeInt` wich
+    requires a `Block<T>(p)`.
+
+*/
+
+/* Rust code:
+
+fn read_write() -> i32 {
+    let mut s1 = Box::new(0); // Allocate memory on the heap and
+                              // it is immidiately initialized
+    let res: i32;
+
+    *s1 = 42;
+
+    res = *s1;
+
+    mem::drop(s1); // Free memory
+
+    res
+}
+
+*/
+
+
+// Allocates an uninitialized integer in head. 
+extern int *mallocInt ();
+/*@ spec mallocInt();
+    requires true;
+    ensures take v = Block<int>(return);
+@*/
+
+// Deallocates an integer. 
+extern void freeInt (int *p);
+/*@ spec freeInt(pointer p);
+    requires take v = Block<int>(p);
+    ensures true;
+@*/
+
+int read_write()
+{
+  int* s1 = mallocInt();
+  int res;
+
+  // res = *s1; // Fail, becasue s1 is not initilaized
+
+  *s1 = 42; // Can write thanks to `Block<T>(p)` permission.
+  // After writting we have `Owned<T>(p)` permission.
+
+  res = *s1; // Succedes, now s1 is initialized
+
+  freeInt(s1);
+
+  return res;
+}
+
+int main(){
+  read_write(); // ignore return
+}