smackers / smack

SMACK Software Verifier and Verification Toolchain
http://smackers.github.io
Other
432 stars 82 forks source link

Some Rust `Box` operation is internally supported by rustc #777

Open shaobo-he opened 2 years ago

shaobo-he commented 2 years ago

Consider this program,

// An example from `The Little MLer` chapter 3
#[macro_use]
extern crate smack;
use smack::*;
//#[derive(Debug)]
enum Pizza {
    Crust,
    Cheese(Box<Pizza>),
    Onion(Box<Pizza>),
    Anchovy(Box<Pizza>),
    Sausage(Box<Pizza>),
}
fn make_plain_pizza() -> Pizza {
    Pizza::Crust
}
fn cheese_it_up(pizza: Pizza) -> Pizza {
    Pizza::Cheese(Box::new(pizza))
}
fn add_salt(pizza: Pizza) -> Pizza {
    Pizza::Anchovy(Box::new(pizza))
}
fn remove_anchovy(pizza: Pizza) -> Pizza {
    match pizza {
        Pizza::Crust => pizza,
        Pizza::Cheese(p) => Pizza::Cheese(Box::new(remove_anchovy(*p))),
        Pizza::Onion(p) => Pizza::Onion(Box::new(remove_anchovy(*p))),
        Pizza::Anchovy(p) => remove_anchovy(*p),
        Pizza::Sausage(p) => Pizza::Sausage(Box::new(remove_anchovy(*p))),
    }
}
fn contains_anchovy(pizza: &Pizza) -> bool {
    match pizza {
        Pizza::Crust => false,
        Pizza::Cheese(p) => contains_anchovy(&*p),
        Pizza::Onion(p) => contains_anchovy(&*p),
        Pizza::Anchovy(p) => true,
        Pizza::Sausage(p) => contains_anchovy(&*p),
    }
}
fn main() {
    println!("Hello, world!");
    let salt_double_cheese_pizza = cheese_it_up(add_salt(
                                       cheese_it_up(make_plain_pizza())));
    //println!("{:?}", salt_double_cheese_pizza);
    //assert!(contains_anchovy(&remove_anchovy(salt_double_cheese_pizza)));
    smack::assert!(contains_anchovy(&remove_anchovy(salt_double_cheese_pizza)));
}

SMACK's Box implementation fails to type check with the following message,

error[E0507]: cannot move out of dereference of `smack::Box<Pizza>`
  --> ml.rs:25:67
   |
25 |         Pizza::Cheese(p) => Pizza::Cheese(Box::new(remove_anchovy(*p))),
   |                                                                   ^^ move occurs because value has type `Pizza`, which does not implement the `Copy` trait

It seems *Box<T> is not (cannot be) desugared into a call to deref but instead is treated uniquely by rustc.

This blog post discusses this issue: https://manishearth.github.io/blog/2017/01/10/rust-tidbits-box-is-special/

zvonimir commented 2 years ago

Can we fix this somehow?