Skip to content
This repository has been archived by the owner on Jul 31, 2023. It is now read-only.

Construct values lazily #33

Open
alastairreid opened this issue Sep 13, 2020 · 1 comment
Open

Construct values lazily #33

alastairreid opened this issue Sep 13, 2020 · 1 comment
Labels
propverify Related to propverify / proptest

Comments

@alastairreid
Copy link
Contributor

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 alastairreid added the propverify Related to propverify / proptest label Sep 13, 2020
@alastairreid
Copy link
Contributor Author

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.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
propverify Related to propverify / proptest
Projects
None yet
Development

No branches or pull requests

1 participant