Skip to content

Commit 5330e09

Browse files
RyanGlScottRyanGlScott
committed
Start a SAW Rust verification tutorial
This patch adds an incomplete tutorial on how to use SAW to verify Rust code, which complements the existing tutorial that covers LLVM and JVM verification. This tutorial currently covers everything that has been implemented in SAW, which includes: * `mir-json` * `mir_verify` basics * References * Arrays * Tuples * Structs * Enums * `mir_fresh_expanded_value` * Slices * Overrides * Statics The final section of the tutorial describes a case study using SAW to verify a real-world piece of Rust code that implements the Salsa20 stream cipher. Related to #1859. [ci skip]
1 parent 63093c3 commit 5330e09

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

82 files changed

+4871
-4
lines changed

‎CONTRIBUTING.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ The top-level repository directories are:
6565

6666
* `saw` - Source for the `saw` executable interpreter for SAWScript.
6767

68-
* `doc` - A tutorial and manual for SAWScript.
68+
* `doc` - A manual and tutorials for SAWScript.
6969

7070
* `examples` - Various examples of using SAWScript.
7171

‎README.md

+10-3
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,17 @@ incomplete support for the Rust language.
1111

1212
## Documentation
1313

14-
The [SAWScript tutorial](https://saw.galois.com/tutorial.html) gives an
15-
introduction to using the SAWScript interpreter. A longer
14+
There are two SAWScript tutorials that give an introduction to using the
15+
SAWScript interpreter:
16+
17+
* [This tutorial](https://saw.galois.com/tutorial.html) gives an
18+
introduction to verifying C code (using LLVM) and Java code (using JVM).
19+
* [This tutorial](https://github.com/GaloisInc/saw-script/blob/master/doc/rust-tutorial/rust-tutorial.md)
20+
gives an introduction to verifying Rust code (using MIR).
21+
22+
There is also a longer
1623
[manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md)
17-
describes the breadth of SAWScript's features.
24+
that describes the breadth of SAWScript's features.
1825

1926
## Precompiled Binaries
2027

‎doc/rust-tutorial/Makefile

+66
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
TARGET = tmp/sawScriptRustTutorial
2+
SRCS = ${TARGET}.md ${wildcard *.bib} ${wildcard *.cls} ${wildcard *.sty}
3+
CODE = ${wildcard code/*.c} \
4+
${wildcard code/*.cry} \
5+
${wildcard code/*.java} \
6+
${wildcard code/*.saw}
7+
TARBALL = tmp/saw-rust-tutorial-code.tar.gz
8+
SPELLSRC = ${TARGET}.tex
9+
NEWSPELL = ${TARGET}.SPELLNEW
10+
OLDSPELL = ${TARGET}.SPELLOLD
11+
SPELL = aspell -t -l
12+
AUX = ${wildcard *.blg} ${wildcard *.bbl} ${wildcard *.aux} \
13+
${wildcard *.eps} ${wildcard *.log} ${wildcard *.toc} \
14+
${TARGET}.md
15+
PDFARGS = -H rust-tutorial-head.tex \
16+
-B rust-tutorial-before.tex \
17+
-A rust-tutorial-after.tex \
18+
--toc \
19+
--listings \
20+
-V documentclass:galois-whitepaper \
21+
-V fontsize:12 \
22+
--pdf-engine=xelatex
23+
HTMLARGS = --css doc.css \
24+
-B rust-tutorial-before.html \
25+
--toc \
26+
--standalone \
27+
--metadata title="SAWScript Rust Tutorial" \
28+
--self-contained
29+
30+
all: ${TARGET}.pdf ${TARGET}.html ${TARBALL}
31+
32+
${TARGET}.pdf: ${SRCS} Makefile | tmp
33+
pandoc ${PDFARGS} -o $@ ${TARGET}.md
34+
35+
${TARGET}.html: ${SRCS} Makefile | tmp
36+
pandoc ${HTMLARGS} -o $@ ${TARGET}.md
37+
38+
${TARBALL}: ${CODE}
39+
tar czf ${TARBALL} code
40+
41+
# Pre-processing step. Right now, does nothing.
42+
${TARGET}.md: rust-tutorial.md docode.hs ${CODE} | tmp
43+
runhaskell docode.hs < $< > $@
44+
45+
docode: ${TARGET}.md | tmp
46+
47+
.PHONY: spellClean superClean clean quickSpell
48+
49+
tmp:
50+
mkdir -p tmp
51+
52+
clean:
53+
-rm -f ${AUX}
54+
55+
superClean: clean
56+
-rm -f ${TARGET}.pdf ${TARGET}.html ${TARGET}.md tmp
57+
58+
spellClean:
59+
rm -f ${NEWSPELL} ${OLDSPELL}
60+
61+
quickSpell:
62+
@touch ${NEWSPELL}
63+
@mv -f ${NEWSPELL} ${OLDSPELL}
64+
@cat ${SPELLSRC} | ${SPELL} | tr "A-Z" "a-z" | sort | uniq | less > ${NEWSPELL}
65+
@echo '(The ones marked with < are new.)'
66+
@diff ${NEWSPELL} ${OLDSPELL}

‎doc/rust-tutorial/README.md

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
To update the tutorial, edit `rust-tutorial.md` and then run `make`. The output
2+
is generated in `./tmp`. If you want to version a new copy of the tutorial,
3+
copy `./tmp/sawScriptRustTutorial.pdf` to `./sawScriptRustTutorial.pdf` and
4+
commit.
5+
6+
Note that some uses of the `^` character in this tutorial cause problems with
7+
especially old versions of `pandoc`. I have confirmed that the tutorial builds
8+
successfully with `pandoc 2.17.1.1` or later.

‎doc/rust-tutorial/code/.gitignore

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
tmp
2+
3+
*.exe
4+
*.mir
5+
*.rlib
6+
7+
first-example
8+
generics-take-1
9+
generics-take-2
10+
saw-basics

‎doc/rust-tutorial/code/Makefile

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
RS_FILES := $(wildcard *.rs)
2+
JSON_FILES := $(RS_FILES:.rs=.linked-mir.json)
3+
EXE_FILES := $(RS_FILES:.rs=)
4+
5+
all: $(JSON_FILES)
6+
7+
%.linked-mir.json: %.rs
8+
saw-rustc $<
9+
$(MAKE) remove-unused-build-artifacts
10+
11+
.PHONY: remove-unused-build-artifacts
12+
remove-unused-build-artifacts:
13+
rm -f test lib*.mir lib*.rlib $(EXE_FILES)
14+
15+
.PHONY: clean
16+
clean: remove-unused-build-artifacts
17+
rm -f *.linked-mir.json

‎doc/rust-tutorial/code/arrays-fail.saw

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
enable_experimental;
2+
3+
let index_fail_spec = do {
4+
arr <- mir_fresh_var "arr" (mir_array 3 mir_u32);
5+
idx <- mir_fresh_var "idx" mir_usize;
6+
7+
mir_execute_func [mir_term arr, mir_term idx];
8+
9+
mir_return (mir_term {{ arr @ idx }});
10+
};
11+
12+
m <- mir_load_module "arrays.linked-mir.json";
13+
14+
mir_verify m "arrays::index" [] false index_fail_spec z3;

‎doc/rust-tutorial/code/arrays.linked-mir.json

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::d8c12f833d14aeb7"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::usize"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}},"pos":"arrays.rs:6:10: 6:13","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::usize"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"}},"pos":"arrays.rs:6:6: 6:14","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"3"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"}},"pos":"arrays.rs:6:6: 6:14","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"}},"kind":"Copy"},"kind":"BinaryOp","op":{"kind":"Lt"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"}},"kind":"Move"},"expected":true,"kind":"Assert","msg":"index out of bounds: the length is move _4 but the index is _3","pos":"arrays.rs:6:6: 6:14","target":"bb1"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"arrays.rs:6:5: 6:14","rhs":{"kind":"CopyForDeref","place":{"data":[{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::d8c12f833d14aeb7"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"arrays.rs:6:5: 6:14","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"arrays.rs:7:2: 7:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"arrays/f3339ccb::index_ref_arr","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::30b61a0858282572"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::usize"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}},"pos":"arrays.rs:2:9: 2:12","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::usize"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"}},"pos":"arrays.rs:2:5: 2:13","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"3"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"}},"pos":"arrays.rs:2:5: 2:13","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"}},"kind":"Copy"},"kind":"BinaryOp","op":{"kind":"Lt"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"}},"kind":"Move"},"expected":true,"kind":"Assert","msg":"index out of bounds: the length is move _4 but the index is _3","pos":"arrays.rs:2:5: 2:13","target":"bb1"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"arrays.rs:2:5: 2:13","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::30b61a0858282572"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"arrays.rs:3:2: 3:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::bool"}]},"name":"arrays/f3339ccb::index","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"arrays/f3339ccb::index_ref_arr","kind":"Item","substs":[]},"name":"arrays/f3339ccb::index_ref_arr"},{"inst":{"def_id":"arrays/f3339ccb::index","kind":"Item","substs":[]},"name":"arrays/f3339ccb::index"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::Array::d8c12f833d14aeb7","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"3"},"ty":"ty::usize"},"ty":"ty::Ref::e028c0f25e8b6323"}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::Array::30b61a0858282572","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"3"},"ty":"ty::usize"},"ty":"ty::u32"}}],"roots":["arrays/f3339ccb::index","arrays/f3339ccb::index_ref_arr"]}

‎doc/rust-tutorial/code/arrays.rs

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
pub fn index(arr: [u32; 3], idx: usize) -> u32 {
2+
arr[idx]
3+
}
4+
5+
pub fn index_ref_arr(arr: [&u32; 3], idx: usize) -> u32 {
6+
*arr[idx]
7+
}

‎doc/rust-tutorial/code/arrays.saw

+33
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
enable_experimental;
2+
3+
let index_spec = do {
4+
arr <- mir_fresh_var "arr" (mir_array 3 mir_u32);
5+
idx <- mir_fresh_var "idx" mir_usize;
6+
mir_precond {{ 0 <= idx }}; // Lower bound of idx
7+
mir_precond {{ idx <= 2 }}; // Upper bound of idx
8+
9+
mir_execute_func [mir_term arr, mir_term idx];
10+
11+
mir_return (mir_term {{ arr @ idx }});
12+
};
13+
14+
m <- mir_load_module "arrays.linked-mir.json";
15+
16+
mir_verify m "arrays::index" [] false index_spec z3;
17+
18+
let index_alt_spec = do {
19+
arr0 <- mir_fresh_var "arr0" mir_u32;
20+
arr1 <- mir_fresh_var "arr1" mir_u32;
21+
arr2 <- mir_fresh_var "arr2" mir_u32;
22+
let arr = mir_array_value mir_u32 [mir_term arr0, mir_term arr1, mir_term arr2];
23+
24+
idx <- mir_fresh_var "idx" mir_usize;
25+
mir_precond {{ 0 <= idx }}; // Lower bound of idx
26+
mir_precond {{ idx <= 2 }}; // Upper bound of idx
27+
28+
mir_execute_func [arr, mir_term idx];
29+
30+
mir_return (mir_term {{ [arr0, arr1, arr2] @ idx }});
31+
};
32+
33+
mir_verify m "arrays::index" [] false index_alt_spec z3;

‎doc/rust-tutorial/code/enums.linked-mir.json

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Deinit","pos":"enums.rs:6:5: 6:9"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"enums.rs:6:5: 6:9","variant_index":0}],"terminator":{"kind":"Return","pos":"enums.rs:7:2: 7:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}]},"name":"enums/caeb2906::i_got_nothing","return_ty":"ty::Adt::3fa7c2d95c7fce06","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"enums.rs:11:2: 11:2"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"enums/caeb2906::do_stuff_with_option","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"enums.rs:2:10: 2:11","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Deinit","pos":"enums.rs:2:5: 2:12"},{"kind":"Assign","lhs":{"data":[{"kind":"Downcast","variant":1},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"enums.rs:2:5: 2:12","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"enums.rs:2:5: 2:12","variant_index":1}],"terminator":{"kind":"Return","pos":"enums.rs:3:2: 3:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}]},"name":"enums/caeb2906::i_found_something","return_ty":"ty::Adt::3fa7c2d95c7fce06","spread_arg":null}],"adts":[{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::option::Option::_adtc5e93708b8ca6e2a[0]","orig_def_id":"core/73237d41::option::Option","orig_substs":["ty::u32"],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::option::Option::None"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::option::Option::Some::0","ty":"ty::u32"}],"inhabited":true,"name":"core/73237d41::option::Option::Some"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"enums/caeb2906::i_got_nothing","kind":"Item","substs":[]},"name":"enums/caeb2906::i_got_nothing"},{"inst":{"def_id":"enums/caeb2906::do_stuff_with_option","kind":"Item","substs":[]},"name":"enums/caeb2906::do_stuff_with_option"},{"inst":{"def_id":"enums/caeb2906::i_found_something","kind":"Item","substs":[]},"name":"enums/caeb2906::i_found_something"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Adt::3fa7c2d95c7fce06","ty":{"kind":"Adt","name":"core/73237d41::option::Option::_adtc5e93708b8ca6e2a[0]","orig_def_id":"core/73237d41::option::Option","substs":["ty::u32"]}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}}],"roots":["enums/caeb2906::i_found_something","enums/caeb2906::i_got_nothing","enums/caeb2906::do_stuff_with_option"]}

‎doc/rust-tutorial/code/enums.rs

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
pub fn i_found_something(x: u32) -> Option<u32> {
2+
Some(x)
3+
}
4+
5+
pub fn i_got_nothing() -> Option<u32> {
6+
None
7+
}
8+
9+
pub fn do_stuff_with_option(o: Option<u32>) {
10+
// ...
11+
}

‎doc/rust-tutorial/code/enums.saw

+35
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
enable_experimental;
2+
3+
m <- mir_load_module "enums.linked-mir.json";
4+
5+
option_u32 <- mir_find_adt m "core::option::Option" [mir_u32];
6+
7+
let i_found_something_spec = do {
8+
x <- mir_fresh_var "x" mir_u32;
9+
10+
mir_execute_func [mir_term x];
11+
12+
let ret = mir_enum_value option_u32 "Some" [mir_term x];
13+
mir_return ret;
14+
};
15+
16+
mir_verify m "enums::i_found_something" [] false i_found_something_spec z3;
17+
18+
let i_got_nothing_spec = do {
19+
mir_execute_func [];
20+
21+
let ret = mir_enum_value option_u32 "None" [];
22+
mir_return ret;
23+
};
24+
25+
mir_verify m "enums::i_got_nothing" [] false i_got_nothing_spec z3;
26+
27+
let do_stuff_with_option_spec = do {
28+
o <- mir_fresh_expanded_value "o" (mir_adt option_u32);
29+
30+
mir_execute_func [o];
31+
32+
// ...
33+
};
34+
35+
mir_verify m "enums::do_stuff_with_option" [] false do_stuff_with_option_spec z3;

‎doc/rust-tutorial/code/first-example.linked-mir.json

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u8"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u8"}},"pos":"first-example.rs:2:5: 2:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u8"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"first-example.rs:3:2: 3:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u8"}]},"name":"first_example/abef32c5::id_u8","return_ty":"ty::u8","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"first_example/abef32c5::id_u8","kind":"Item","substs":[]},"name":"first_example/abef32c5::id_u8"}],"tys":[{"name":"ty::u8","ty":{"kind":"Uint","uintkind":{"kind":"U8"}}}],"roots":["first_example/abef32c5::id_u8"]}

‎doc/rust-tutorial/code/first-example.rs

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
pub fn id_u8(x: u8) -> u8 {
2+
x
3+
}

‎doc/rust-tutorial/code/generics-take-1.linked-mir.json

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"fns":[],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[],"tys":[],"roots":[]}

‎doc/rust-tutorial/code/generics-take-1.rs

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
pub fn id<A>(x: A) -> A {
2+
x
3+
}

‎doc/rust-tutorial/code/generics-take-2.linked-mir.json

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u8"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u8"}},"pos":"generics-take-2.rs:6:8: 6:9","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u8"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u8"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u8"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::e7e83e5417e656c7"},"kind":"Constant"},"kind":"Call","pos":"generics-take-2.rs:6:5: 6:10"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"generics-take-2.rs:7:2: 7:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u8"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u8"}]},"name":"generics_take_2/8b1bf337::id_u8","return_ty":"ty::u8","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u8"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u8"}},"pos":"generics-take-2.rs:2:5: 2:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u8"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"generics-take-2.rs:3:2: 3:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u8"}]},"name":"generics_take_2/8b1bf337::id::_instaddce72e1232152c[0]","return_ty":"ty::u8","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"generics_take_2/8b1bf337::id_u8","kind":"Item","substs":[]},"name":"generics_take_2/8b1bf337::id_u8"},{"inst":{"def_id":"generics_take_2/8b1bf337::id","kind":"Item","substs":["ty::u8"]},"name":"generics_take_2/8b1bf337::id::_instaddce72e1232152c[0]"}],"tys":[{"name":"ty::u8","ty":{"kind":"Uint","uintkind":{"kind":"U8"}}},{"name":"ty::FnDef::e7e83e5417e656c7","ty":{"defid":"generics_take_2/8b1bf337::id::_instaddce72e1232152c[0]","kind":"FnDef"}}],"roots":["generics_take_2/8b1bf337::id_u8"]}

0 commit comments

Comments
 (0)