Comments regarding setup procedure about vigor HOT 2 CLOSED

It might be a good idea to mention also the amount of disk space needed (along with the amount of RAM) in the requirements (10 GB was not enough, 20 GB has worked).

Done, thanks.

Several steps in the execution of setup.sh seem to require sudo privileges. It would be good to mention it in the README, to avoid letting it run overnight and finding out in the morning that it needed a password to continue ;-) .

Done, thanks.

Why is it needed to rebuild gcc, binutils, etc.? Are there modifications in them?

We need to do cross-compilation for the NFOS. @matrizzo can explain more here, he was in charge of the NFOS part.

Why are the modifications to VeriFast and KLEE maintained in local repositories and not upstreamed?

Because we haven't put in the time to upstream them :-)

It seems that the Makefiles always cause the code to be recompiled (i.e. even if they exist and are up to date). Is that intentional?

Kind of. DPDK has a complex set of Makefiles, and we add our own complex stuff on top, to keep our sanity we always build from scratch to ensure nothing weird happens.

Is it because of my VM only having 8 GB of RAM?

Yes, as mentioned in the README you need 128GB of RAM. (The actual number is probably a bit less, something like 90, but we say 128 to be sure)

It's good to know you were about do symbex/validate the NFs only with 8GB, I've updated the readme to reflect this.

from vigor.

Why are the modifications to VeriFast and KLEE maintained in local repositories and not upstreamed?

Because we haven't put in the time to upstream them :-)

Fair enough :-)

It seems that the Makefiles always cause the code to be recompiled (i.e. even if they exist and are up to date). Is that intentional?

Kind of. DPDK has a complex set of Makefiles, and we add our own complex stuff on top, to keep our sanity we always build from scratch to ensure nothing weird happens.

Indeed, I can understand that, Makefiles can be messy :-/

Is it because of my VM only having 8 GB of RAM?

Yes, as mentioned in the README you need 128GB of RAM. (The actual number is probably a bit less, something like 90, but we say 128 to be sure)

Ah OK. I had understood that only symbex-withnfos would require 128GB. My bad.

It's good to know you were about do symbex/validate the NFs only with 8GB, I've updated the readme to reflect this.

Thank you for your quick response!

from vigor.