'anomaly: Failure("stackify is not compiled")' error message

[safinaskar]

Hi. After several try-and-error steps I was able to create Dockerfile, which installs creusot. Here it is:

FROM debian:bullseye
ENV LC_ALL C.UTF-8
RUN apt-get update && apt-get install -y apt-utils gcc curl less nano mc whiptail locales man-db wget procps sudo apt-file pkg-config

# User
RUN useradd --create-home --uid 1000 --shell /bin/bash user
RUN echo 'user ALL=(ALL) NOPASSWD: ALL' > /etc/sudoers.d/a
USER user
WORKDIR /home/user

# Rust
RUN curl --proto '=https' --tlsv1.2 https://sh.rustup.rs -sSf | bash -s -- -y --default-toolchain none
RUN . "$HOME/.cargo/env"; rustup toolchain install nightly --allow-downgrade

USER root
RUN apt-get update && apt-get install -y git
USER user

RUN . "$HOME/.cargo/env"; mkdir ~/opt && cd ~/opt && git clone https://github.com/xldenis/creusot && creusot/build

USER root
RUN apt-get update && apt-get install -y make bubblewrap
USER user

RUN mkdir ~/bin && wget https://github.com/ocaml/opam/releases/download/2.1.2/opam-2.1.2-x86_64-linux -O ~/bin/opam && chmod +x ~/bin/opam
ENV PATH /home/user/bin:/usr/local/bin:/usr/bin:/bin
RUN opam init --auto-setup --disable-sandboxing

RUN opam pin --confirm-level=unsafe-yes add why3 https://gitlab.inria.fr/why3/why3.git
RUN opam install --confirm-level=unsafe-yes why3 why3-ide

USER root
RUN apt-get update && apt-get install -y z3
USER user

RUN eval $(opam env); why3 config detect

RUN echo 'fn main(){}' > ~/a.rs
RUN . "$HOME/.cargo/env"; eval $(opam env); ~/opt/creusot/mlcfg ~/a.rs > ~/a.mlcfg
RUN . "$HOME/.cargo/env"; eval $(opam env); ~/opt/creusot/prove -P z3 ~/a.mlcfg # This line fails

(By the way it would be good if you will provide similar Dockerfile or at least automatic install script.)

Okey, so I created this Dockerfile and it doesn't work. The very last line fails with message anomaly: Failure("stackify is not compiled")

[xldenis]

Hi @safinaskar, the issue is that you need to ensure that why3 is compiled with support for stackify. This is conditional on the presence of ocamlgraph. if you add ocamlgraph to your install command it will work 'magically' :)

I'm curious, are you exploring using Creusot for anything particular?

[xldenis]

(By the way it would be good if you will provide similar Dockerfile or at least automatic install script.)

You're right, for the moment we only provide the README, but we should really provide an install script that sets up why3 according to our needs. Additionally I need to polish cargo creusot so you can use that instead (it should work, I just don't test it enough).

[xldenis]

You'll find that there is one final issue: you need to generate the libcreusot_contracts.cmeta file, the easiest way atm is to run cargo test --test ui "zzzzzzzz" (the first thing the test suite does is generate the file).

[safinaskar]

Thanks a lot! Now it works after installing ocamlgraph.

You'll find that there is one final issue: you need to generate the libcreusot_contracts.cmeta file, the easiest way atm is to run cargo test --test ui "zzzzzzzz" (the first thing the test suite does is generate the file).

Checking works without this command. find ~/opt/creusot/ -name libcreusot_contracts.cmeta prints /home/user/opt/creusot/target/debug/libcreusot_contracts.cmeta, i. e. the file exists.

I'm curious, are you exploring using Creusot for anything particular?

No. I simply chose Rust as my primary language for all my projects, including both system programming tasks and toy provers. Here is my argument why I chose Rust over Haskell (I know Haskell, too) even for provers: https://zerobin.net/?e8a82c7c6141bb35#jRpw57q2uSxgbXyPjCVuf5tWw+5vdkNSarm4a5mDKx4= .

And I need some tool to verify my Rust code. For example, to make sure that unwrap in some particular place will never fail.

I tried https://github.com/viperproject/prusti-dev , but I didn't like it. Prusti was not able to check that assert will succeed in this code:

a[i] = x; // a is slice
assert!(a[i] == x);

I hope creusot will handle this code. If creusot turns out to be good, I will use it in my various projects

[xldenis]

At the moment that code would work for a : Vec<T>, we were missing a minor feature to specify slices, which now exists (extern_spec), thanks for reminding me I need to add specs for slices.

[xldenis]

With that example, assuming you can show that i is inbounds of the vector/slice the assertion will pass.

Take a look at the vector examples to see what we can do . If you find you are missing specific functions to prove your code let me know, they should be trivial to add but I'd rather do it incrementally.

You can also take a look at vec.rs to see what exists atm.

[safinaskar]

@xldenis Slices still don't work. I use current master (73efc7bb3e428c432b23bac0116f4f08d94ed70d). My code:

extern crate creusot_contracts;

fn f(a: &[i32]) {
}

fn main(){
}

Result:

user@916292dea09c:~/opt/creusot$ ~/opt/creusot/mlcfg ~/a.rs > ~/a.mlcfg
    Finished dev [unoptimized + debuginfo] target(s) in 0.04s
     Running `target/debug/creusot-rustc -Zno-codegen --extern creusot_contracts=./target/debug/libcreusot_contracts.rlib -Ldependency=./target/debug/deps/ --crate-type=lib /home/user/a.rs`
user@916292dea09c:~/opt/creusot$ ~/opt/creusot/prove -P z3 ~/a.mlcfg
File "/home/user/a.mlcfg", line 29, characters 29-34:
unbound type symbol 'array'

Generated a.mlcfg:

a.mlcfg

``` module Type use Ref use mach.int.Int use prelude.Int8 use prelude.Int16 use mach.int.Int32 use mach.int.Int64 use prelude.UInt8 use prelude.UInt16 use mach.int.UInt32 use mach.int.UInt64 use string.Char use floating_point.Single use floating_point.Double use prelude.Prelude end module CreusotContracts_Logic_Resolve_Resolve_Resolve_Interface type self predicate resolve (self : self) end module CreusotContracts_Logic_Resolve_Resolve_Resolve type self predicate resolve (self : self) end module A_F_Interface use prelude.Prelude use mach.int.Int use mach.int.Int32 val f [@cfg:stackify] (a : array int32) : () end module A_F use prelude.Prelude use mach.int.Int use mach.int.Int32 clone CreusotContracts_Logic_Resolve_Resolve_Resolve as Resolve0 with type self = array int32 let rec cfg f [@cfg:stackify] (a : array int32) : () = var _0 : (); var a_1 : array int32; { a_1 <- a; goto BB0 } BB0 { _0 <- (); assume { Resolve0.resolve a_1 }; return _0 } end module A_Main_Interface val main [@cfg:stackify] () : () end module A_Main let rec cfg main [@cfg:stackify] () : () = var _0 : (); { goto BB0 } BB0 { _0 <- (); return _0 } end ```

[xldenis]

Slices still don't work. I use current master

That's expected, as I said above, and in #284, we don't currently support slices. Nothing major missing to do it, but just haven't yet. I'll try to fix it during the week.

[safinaskar]

Thanks a lot

[xldenis]

295 adds basic support for slices: it can translate the type, index immutably and mutably as well as get the length of a slice.

It does not yet add support for creating a slice, but I'll add that in a future PR.

[xldenis]

I'm going to close this for now, but please open up new issues if you encounter missing APIs or further errors.