Poulet4 ccomp v1 runtime

[nikaido-shinku]

run make install, and you should be able to run petr4 compile -I ./examples ./examples/helloWorld.p4 . Currently it is saying that top4cub is raising an error. But after some debugging, we should be able to get a c file from a p4file. I'll finish up the translation of packet.extract.

Details for the reviewer: the main problem was that compcert uses a different extract rule than petr4, which was the reason why I had to move the Ccomp's extraction to a separate directory. However, this makes the extracted ocaml file expecting a different AST than the one petr4 produces. So I had to create one intermediate pass to glue the two AST together.

TODO: We should write a simple v1model main function, however, I didn't really understand how we should handle the copy-in copy-out of the standard metadata. It will be really helpful if someone can take a look at this.

[nikaido-shinku]

Also it would be great if someone professional in Compcert can give me some input on "compcertalize.ml" file's first few functions. Please let me know if converting bigint into string and then converting into coq numbers looks like a terrible idea at first sight.

[nikaido-shinku]

And it would be great if eric can look into the error I encountered, since you are more familiar with toP4cub than I am. The command was petr4 compile -I ./examples ./examples/helloWorld.p4

[ericthewry]

You can add error reporting for better error messages by modifying lib/common.ml. Change this line to something like

| Poulet4.Result.Result.Error msg -> failwith ("error occured in ToP4cub: " ^ msg)

This will give you an error like the following

error occurred in ToP4cub: [FIXME] integer didnt have a width.

which indicates that you need to add a width to the constant in helloworld.p4. That is, change 9 to 9w9.

[nikaido-shinku]

I can compile a p4 file into a .o file provided that the p4file does not have struct with same types. However, when I run the executable, there's a segmentation fault.