search

cornell-netlab / p4check

P4Check 16: A Static Analysis tool for P4 16 that detects accesses to invalid headers
https://doi.org/10.4230/LIPIcs.ECOOP.2019.12
7 stars 0 forks source link

hello，I would like to ask you some questions #2

Open libinnnn opened 4 years ago

libinnnn commented 4 years ago

I find that you are a bit different from the p4-check tool. The p4-check tool used before can also perform complete static data detection of p4 code. Is the source code of this p4v tool in your laboratory open source?

jnfoster commented 4 years ago

No. The p4v tool is owned by Barefoot, now a part of Intel.

libinnnn commented 4 years ago

Hello, I have encountered many problems in setting up the environment according to the tutorial. After opam installed dune. "Error: Version 1.9 of dune is not supported." Will appear when using the make command. I don't know if you can provide a docker environment that has been built for testing

ericthewry commented 4 years ago

can you provide more detail?

jnfoster commented 4 years ago

It sounds like you should upgrade your Dune installation. I recommend installing everything OCaml related through the OPAM package manager, including Dune.

Putting together a Docker image is an interesting idea. But we probably don't have time to take that on for now...

libinnnn commented 4 years ago

Thank you for your suggestion. After updating opam, I can successfully use p4-check, but I have encountered new problems. The information prompting me is as follows `Uncaught exception:

(Failure "could not find packagemain")

Raised at file "stdlib.ml", line 33, characters 17-33 Called from file "lib/p4check.ml", line 1649, characters 38-64 Called from file "bin/main.ml", line 57, characters 18-48 Called from file "src/command.ml", line 2817, characters 8-205 Called from file "src/exn.ml", line 107, characters 6-10` The p4 code I use is based on the tofino model, but the use case you gave is based on v1model. Will this affect the tool detection?

jnfoster commented 4 years ago

Yes, the front-end only supports V1Model.

Now that TNA has been opened we can work on that.

libinnnn commented 4 years ago

I read your code, and I want to modify the code to support the tofino model, to further verify the ability of p4-check for message verification, can I add your Twitter to communicate briefly?

ericthewry commented 4 years ago

sure, my handle is the same.

libinnnn commented 4 years ago

It's very sad that I can't seem to have a private message on Twitter, or can I add your facebook account, this seems to be more convenient for communication

jnfoster commented 4 years ago

Email is best for me, and I suspect @ericthewry too. (I don't keep track of social media inboxes carefully.)

Our address can be found on our web pages, which are linked to from our GitHub profiles.

libinnnn commented 4 years ago

OK，thank you