vigor-nf / vigor Goto Github PK

These are a few comments that I collected while following the README to setup an environment to reproduce verifications.
My configuration:

• VirtualBox
• Ubuntu 18.04 LTS
• VM with 4 CPUs, 8 GB RAM (can't really allocate more, my machine has 16GB total...)
  I ran setup.sh without argument.

Here are the comments and questions:

• 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).
• 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 ;-) .
• Why is it needed to rebuild gcc, binutils, etc.? Are there modifications in them?
• Why are the modifications to VeriFast and KLEE maintained in local repositories and not upstreamed?
• 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?
• I was able to run make symbex validate for all NFs, but trying make symbex-withdpdk fails as follows:

Command terminated by signal 9
	Command being timed: "klee -no-externals -allocate-determ -allocate-determ-start-address=0x00040000000 -allocate-determ-size=1000 -dump-call-traces -dump-call-trace-prefixes -solver-backend=z3 -exit-on-error -max-memory=750000 -search=dfs -condone-undeclared-havocs --debug-report-symbdex nf.bc --no-shconf -- --lan-dev 0 --wan 1 --eth-dest 0,01:23:45:67:89:00 --eth-dest 1,01:23:45:67:89:01"
	User time (seconds): 112.87
	System time (seconds): 7.11
	Percent of CPU this job got: 78%
	Elapsed (wall clock) time (h:mm:ss or m:ss): 2:33.01
	Average shared text size (kbytes): 0
	Average unshared data size (kbytes): 0
	Average stack size (kbytes): 0
	Average total size (kbytes): 0
	Maximum resident set size (kbytes): 7911708
	Average resident set size (kbytes): 0
	Major (requiring I/O) page faults: 74075
	Minor (reclaiming a frame) page faults: 2206267
	Voluntary context switches: 75022
	Involuntary context switches: 4896
	Swaps: 0
	File system inputs: 17900776
	File system outputs: 534472
	Socket messages sent: 0
	Socket messages received: 0
	Signals delivered: 0
	Page size (bytes): 4096
	Exit status: 0

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

• I had also some comments on the documentation for the specification language in doc/SpecificationSemantics.md, for which I opened #1.

Feel free to answer here, or at your convenience we can setup a meeting to discuss in more details, let me know.

Hi

I'd like to verify NFs. However, I'm facing an issue when validating.

Here is what I did:

1. installed a VM with ubuntu 20
2. ran ./setup.sh as root.
3. cd vignat
4. make symbex validate

However, here is the error I get:

ocamlfind: Package `cil' not found
Cannot run Ocamlfind.
make: *** [/home/vboxuser/vigor/vignat/../Makefile:70: autogen] Error 10

In files vigor/vignat/nat_flowmanager.c and vigor/vigfw/fw_flowmanager.c, there are #include "state.h" preprocessing instructions. But I cannot find the state.h file in the repository. Would you please let us know what is inside of this file and where we can get it?