Add documentation and example for quackyducky part of Everparse

README.md

@@ -39,4 +39,12 @@ Indeed, EverParse is part of [Project Everest](https://project-everest.github.io
 `make`
 
 ### Running
-`./bin/qd.exe -help`
+
+Everparse offers two different executables:
+
+* `./bin/qd.exe` (or `quackyducky` when using the Docker file in `./example`): this executable produces parser/serializer pairs in F* given an input description similar to C types.
+
+    An example of use of `quackyducky` is detailed in [this documentation](./example/README.md).
+* `./bin/3d.exe` or (`3d`when using the Docker file in `./example`): this executable produces validators in F* given a description in 3d description language.
+
+    The documentation for this executable can be found [here](https://project-everest.github.io/everparse/3d.html).

example/Dockerfile

@@ -0,0 +1,22 @@
+# BUILD
+## docker build -t customeverparse:everparse .
+
+# START AND RUN
+## docker run --rm -v $PWD:/pwd -d --name customeverparse -i customeverparse:everparse && docker exec -it customeverparse /bin/bash
+
+
+FROM projecteverest/everest-linux
+
+USER root
+
+RUN ln -s /home/test/everparse/bin/qd.exe /bin/quackyducky 
+RUN ln -s /home/test/everparse/bin/3d.exe /bin/3d 
+RUN ln -s /home/test/karamel/krml /bin/krml 
+RUN ln -s /home/test/FStar/bin/fstar.exe /bin/fstar 
+
+USER test
+
+ENV FSTAR_HOME="/home/test/FStar"
+ENV KRML_HOME="/home/test/karamel"
+ENV EVERPARSE_HOME="/home/test/everparse"
+ENV LOWPARSE_HOME="${EVERPARSE_HOME}/src/lowparse"

example/README.md

@@ -0,0 +1,63 @@
+# QuackyDucky example
+
+This documentation is a walkthrough of the `quackyducky` executable that generates parser/serialiser pairs.
+
+`quackyducky` is the compiler that generates parsers, serialisers, lemmas and theorems in F* out of a description of a message format. It is described in details in the [USENIX Security 2019 paper](https://www.microsoft.com/en-us/research/publication/everparse/).
+
+## Walkthrough
+
+First you have to write a description of the format you want the parser/serialiser for. The format is very similar to C structs. The available types and examples can be found in the [USENIX Security 2019 paper](https://www.microsoft.com/en-us/research/publication/everparse/).
+
+
+As an example, here is a description file:
+
+```
+struct {
+    uint16 id;
+    uint32 list<12..42>;
+    uint32 list2<32..234>;
+} content_one;
+
+struct {
+    uint32 size;
+    uint64 a[size];
+} content_two;
+
+enum {
+    one (0x4242), /* Constant tag */
+    two (0x4241),
+    (65535) /* Indicates 16 bit representation */ 
+} content_type; /* Enum with 2 defined cases */ 
+
+struct {
+    uint32 id;
+    content_type c_t;
+    select (c_t){
+        case one: content_one;
+        case two: content_two;
+    } inner_content;
+    uint16 arr[412];
+} message;
+```
+
+Now, run `./build_docker.sh` (`./build_docker.ps1` respectively) to build the docker image.
+
+Once it is done, run `./run_docker.sh` (`./run_docker.ps1` respectively) to start a docker container and open a shell inside.
+
+## Simple example by hand
+
+In the docker container:
+- `cd /pwd/files/simple_example` to go to the `./files/simple_example` folder next to this README file.
+- run `quackyducky -odir code -low specs.qd` command to generate the F* code files in `code` folder. It will generate `.fst` and `.fsti` files that contain the parsers, serialisers and proofs.
+- run `cd code && fstar --z3rlimit 3000 --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse  --include $LOWPARSE_HOME --include $KRML_HOME/krmllib --include $KRML_HOME/krmllib/obj --cmi --expose_interfaces *.fst *.fsti ` to verify the F* code. If the verification times out, you can modify the value of the option `--z3rlimit`.
+
+## Example using `make` to generate C code
+
+In the docker container:
+
+- `cd /pwd/files/make_example` to go to the `./files/make_example` folder next to this README file.
+- run `make clean`
+- fill `specs.qd`
+- run `./generate_code.sh -low` or `./generate_code.sh -high`
+- run `make`
+- C code is output in the `out` folder

example/build_docker.ps1

@@ -0,0 +1 @@
+docker build -t customeverparse:everparse .

example/build_docker.sh

@@ -0,0 +1 @@
+docker build -t customeverparse:everparse .

example/files/make_example/Makefile

@@ -0,0 +1,45 @@
+include Makefile.common
+
+all: verify test
+
+cache/%.checked:
+	$(FSTAR) $(OTHERFLAGS) $<
+	@touch $@
+
+krml/%.krml:
+	$(FSTAR) --codegen krml $(patsubst %.checked,%,$(notdir $<)) --extract_module $(basename $(patsubst %.checked,%,$(notdir $<))) --warn_error '@241'
+	@touch $@
+
+-include .depend
+
+.qd_files: $(QD_FILES)
+	+$(MAKE) -f Makefile.qd_files
+
+.depend: .qd_files
+	+$(MAKE) -f Makefile.depend
+
+depend: .depend
+
+verify: $(patsubst %,cache/%.checked,$(QD_FILES))
+	echo $*
+
+ALL_KRML_FILES := $(filter-out krml/prims.krml,$(ALL_KRML_FILES))
+
+extract: $(ALL_KRML_FILES) # from .depend
+	mkdir -p out
+	$(KRML) -warn-error '@2' -skip-compilation $^
+
+test.exe: $(ALL_KRML_FILES)
+	mkdir -p out
+	$(KRML) $(LOWPARSE_HOME)/LowParse_TestLib_Low_c.c -no-prefix Test $^ -o test.exe
+
+test: test.exe
+	./test.exe
+
+%.fst-in %.fsti-in:
+	@echo $(FSTAR_OPTIONS)
+
+clean:
+	rm -rf .qd_files .depend cache krml out $(filter-out Test.fst,$(QD_FILES)) test.exe
+
+.PHONY: all depend verify extract clean build test

example/files/make_example/Makefile.common

@@ -0,0 +1,15 @@
+FSTAR_OPTIONS = --odir krml --cache_dir cache --cache_checked_modules \
+		--already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse \
+		--include $(LOWPARSE_HOME) --include $(KRML_HOME)/krmllib --include $(KRML_HOME)/krmllib/obj --cmi
+
+FSTAR = $(FSTAR_HOME)/bin/fstar.exe --trace_error $(FSTAR_OPTIONS)
+
+HEADERS = $(addprefix -add-include ,'"krml/internal/compat.h"')
+
+KRML = $(KRML_HOME)/krml \
+	 -ccopt "-Ofast" \
+	 -drop 'FStar.Tactics.\*' -drop FStar.Tactics -drop 'FStar.Reflection.\*' \
+	 -tmpdir out \
+	 -bundle 'LowParse.\*' \
+	 $(HEADERS) \
+	 -warn-error -9

example/files/make_example/Makefile.depend

@@ -0,0 +1,8 @@
+include Makefile.common
+include .qd_files
+
+all:
+	cat .qd_files > .depend
+	$(FSTAR) --dep full $(QD_FILES) >> .depend
+
+.PHONY: all

example/files/make_example/Makefile.qd_files

@@ -0,0 +1,4 @@
+all:
+	echo QD_FILES = $(wildcard *.fst *.fsti) > .qd_files
+
+.PHONY: all

example/files/make_example/generate_code.sh

@@ -0,0 +1 @@
+quackyducky -odir . $1 specs.qd

example/files/make_example/specs.qd

@@ -0,0 +1,5 @@
+struct {
+    uint64 id;
+    uint16 size;
+    uint8 arr[size];
+} message;

example/files/simple_example/specs.qd

@@ -0,0 +1,26 @@
+struct {
+    uint16 id;
+    uint32 list<12..42>;
+    uint32 list2<32..234>;
+} content_one;
+
+struct {
+    uint32 size;
+    uint64 a[size];
+} content_two;
+
+enum {
+    one (0x4242), /* Constant tag */
+    two (0x4241),
+    (65535) /* Indicates 16 bit representation */ 
+} content_type; /* Enum with 2 defined cases */ 
+
+struct {
+    uint32 id;
+    content_type c_t;
+    select (c_t){
+        case one: content_one;
+        case two: content_two;
+    } inner_content;
+    uint16 arr[412];
+} message;

example/run_docker.ps1

@@ -0,0 +1,2 @@
+docker run --rm -v $PWD:/pwd -d --name customeverparse -i customeverparse:everparse
+docker exec -it customeverparse /bin/bash

example/run_docker.sh

@@ -0,0 +1,2 @@
+docker run --rm -v $PWD:/pwd -d --name customeverparse -i customeverparse:everparse
+docker exec -it customeverparse /bin/bash