Newer
Older
# RustLog
## A formalization of the Polonius model checker
- [Presentations PDF directory](pres/pdf/)
- [Logbook](logbook.md)
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
- [Final report](report/main.pdf)
## How to use RustLog
RustLog is a formalization of the Polonius model checker. It is written in Prolog and the rules are available in the [prog.pl](prog.pl) file. To use RustLog, you need to install [SWI-Prolog](https://www.swi-prolog.org/). Then, you can load the rules in the Prolog interpreter with the following command:
```bash
swipl -s prog.pl -s liveness.pl
```
You can then use the predicates defined in the rules to check borrow validity.
### Example
Let's say we have the following program:
```rust
let mut x = 42;
let y = &mut x;
x = 13;
y;
```
We can convert this code to Prolog syntax and use the rules to check the validity of the borrow:
- First define the liveness of the variables in the `liveness.pl` file:
- `liveUntil(x, 3).`
- `liveUntil(y, 4).`
- Then start the Prolog interpreter and load the rules and the liveness files:
```bash
swipl -s prog.pl -s liveness.pl
```
- Finally we can check the validity of the borrow with the `borrowChecker` predicate:
```prolog
borrowChecker([(1, let, mut, x, 42), (2, let, immut, y, mut, x), (3, x, 13), (4, y)], [], CF).
```
The prolog prompt will output the following:
```prolog
?- borrowChecker([(1, let, mut, x, 42), (2, let, immut, y, mut, x), (3, x, 13), (4, y)], [], CF).
Conflict detected at line: 3
Trying to borrow x as mut while it is borrowed as mut by y
true.
```