Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

SMT Arrays #41

Open
filipeom opened this issue Nov 29, 2023 · 4 comments
Open

SMT Arrays #41

filipeom opened this issue Nov 29, 2023 · 4 comments

Comments

@filipeom
Copy link
Member

Model linear memory using arrays

@hra687261
Copy link
Contributor

Do you have any literature/specification on the memory models in question?
Can the SMT theory of sequences be used?

@filipeom
Copy link
Member Author

filipeom commented Jan 27, 2024

The idea behind this is simply to attempt to utilize the array theory presented in Z3 (https://microsoft.github.io/z3guide/docs/theories/Arrays/) to model our linear memory in Wasm. I don't expect this to be that efficient, but we need to compare it against our other models to argue their efficiency.

We could also potentially employ sequences. I would need to investigate further, but with some effort, I believe we could probably make this work :)

Edit: paper https://www.microsoft.com/en-us/research/publication/generalized-efficient-array-decision-procedures/

@hra687261
Copy link
Contributor

Alright. Yes I am familiar with that paper, I was asking about literature/specification, because I was wondering if the basic SMT theory of arrays (with only the select and store operators) would be enough, or the additional operators described in that paper are necessary (like const, map ...)

@filipeom
Copy link
Member Author

Oh, yes, I apologize for the misunderstanding. Sections 2.1.1 and 2.1.2 of this paper provide an overview of what we aim to achieve. And, yes I expect that only 'select' and 'store' operations are necessary.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants