# Theis: A Booster for Building Safer Systems Using the Rust Programming Language
## 4 Design and Construction of Thetis
### Functionally Equivalent Replacement
#### 4.1.2 Replacement of _Union_ Types  
A _union_ is similar to a type _struct_ in terms of definition but allows storing different data types in the same memory location. For this reason, when accessing some fields of a _union_, it may overwrite other data's fields or access undefined memory space, resulting in faults. Therefore, in Thetis, the type _struct_ is used to replace _union_ for optimization. Thetis optimizes the _union_ operations based on feature detection and replacement. We note that the _struct_ syntax is similar in form to the _union_ keyword. The _struct_ can be used in safe code fragments. Therefore, we propose replacing _union_ with _struct_ in safety scenarios. However, direct replacement is quite challenging. In this paper, we propose a framework that offers many equivalent alternatives for the syntax. Firstly, from the perspective of initializing memory languages, in the initialization of _union_, only one of the fields needs to be initialized with a value. The type _struct_, on the other hand, needs to be initialized for all the fields it contains. We achieve this by implementing \"#[derive(Default)]\" for the replaced struct, where each field is first initialized using the default value before being modified based on the initialized fields in the union. Regarding #[derive (Default)], it automatically uses the default trait code for the struct, as shown in Listing 6, assigning default values to each field. ```
#[derive(Default)] structTe{f1:u32,f2:f32};implDefaultforTe{ fndefault()->Self{Self{f1:0,f2:0.0,}} }
```  
Secondly, from the perspective of accessibility, when using the union field multiple times during initialization, the value of each initialization will overwrite the previous memory space. However, struct will retain the results of each assignment. This will result in nonequivalence between the struct and union substitution. To address this issue, we add assertions after replacing the struct fields to prevent access to undefined fields in the union before the replacement, maintaining semantic consistency. To better understand our replacement process, we provide an example, as shown in Listing 7. ```
//Afterreplacement//Beforereplacement#[derive[Default]]unionTe{f1:u32,f2:f32};structTe{f1:u32,f2:f32};letu=Te{f1:1};letu=Te::default();u.f1=1;unsafe{letf=u.f1};letm=Te{f2:2.0};assert_eq1(u.f1=1&&u.f2=Te.default(),true);letm=Te::default();u.f2=2.0;assert_eq1(u.f1=Te.default()&&u.f2=2.0,true);Finally, we consider that the replacement of _union_ with _struct_ directly reduces the use of the \"unsafe\" keyword while also introducing a small memory overhead. We discuss the overheads in Section 5.2. In general, we analyze the equivalence of replacement frameworks from the perspectives of memory layout and accessibility. Although Listing 7 is a simple example, it also shows that the replaced functionality is correct. In this paper, we did not use formal semantic equivalence proof methods to prove complete equivalence, which is too complex. However, our theoretical and practical analyses of the appeal provide us with reasonable support. The purpose of the design of Thetis is to automatically provide recommended safe code, which can replace unsafe code, with the same functionality. ### Interior Unsafe Encapsulation and ACSL Specification

#### 4.2.1 Measures for Dereferencing Raw Pointers

For dereferencing raw pointers, the correctness of the pointed address cannot be guaranteed because it does not always point to a legal address, and the problem exists that many raw pointers point to the same memory space or NULL. In addition, raw pointers do not have an automatic garbage collection mechanism, which may cause undefined behaviors. Also, Rust does not provide the concept of lifetime for raw pointers, and borrow checking is unavailable. A raw pointer that exceeds its actual lifetime may cause a dangling reference (freeing memory but retaining a pointer to it) issue. In general, it is safe to create a raw pointer but unsafe to dereference it.