project-oak / rust-verification-tools

RVT is a collection of tools/libraries to support both static and dynamic verification of Rust programs.
https://project-oak.github.io/rust-verification-tools/
Apache License 2.0
273 stars 37 forks source link

Construct values lazily #33

Open alastairreid opened 3 years ago

alastairreid commented 3 years ago

Lazy construction will work better with concolic execution because it defers path splitting to the point where a value is accessed.

This cannot be done for types like Option But it can possibly be done for abstract Types like BTreeMap - possibly depending mutability?

alastairreid commented 3 years ago

Two directions to take this:

1) Rust's lazy statics potentially have the opposite problem: deferring construction of an object until after a path split - which requires every path to repeat the effort of creating the object for itself. Perhaps the initialize method would help with this?

2) Chopped symbolic execution adds lazy evaluation into KLEE and might be worth investigating.