Merge branch 'internship' into thesis

README.md

@@ -11,19 +11,20 @@ autopilots.
 
 ## Dependencies
 
-* [Coq](https://coq.inria.fr) (tested with version 8.15)
+* [Coq](https://coq.inria.fr) (tested with version 8.16.1)
 * [OCaml](https://github.com/ocaml/ocaml) (tested with version 4.13.1)
 * [OCamlbuild](https://github.com/ocaml/ocamlbuild) (tested with version 0.14.1)
-* [xml-light](https://github.com/ncannasse/xml-light) (tested with version 2.4)
-* [Menhir](http://gitlab.inria.fr/fpottier/menhir) (tested with version 20220210)
-* [Coq-Mathcomp-SSReflect](https://math-comp.github.io) (tested with version 1.15.0)
+* [xml-light](https://github.com/ncannasse/xml-light) (tested with version 2.5)
+* [Menhir](http://gitlab.inria.fr/fpottier/menhir) (tested with version 20230608)
+* [coq-menhirlib](https://gitlab.inria.fr/fpottier/menhir/-/tree/master/coq-menhirlib) (tested with version 20230608)
+* [Coq-Mathcomp-SSReflect](https://math-comp.github.io) (tested with version 1.16.0)
 
 The dependencies can be installed using [OPAM](https://opam.ocaml.org)
 (version 2.0 or later):
 
 ```bash
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq ocamlbuild xml-light menhir coq-mathcomp-ssreflect coq-menhirlib 
+opam install coq ocamlbuild xml-light menhir coq-menhirlib coq-mathcomp-ssreflect 
 ```
 
 To generate the documentation, the package `graphviz` must be installed:
@@ -78,7 +79,10 @@ All the tests available are described [here](./docs/tests.md)
   has been modified to use the function `create_ident` used for the
   verification, `arbitrary_ident` for the definition of `nav_init_stage`
   function and the variable `_t'1` has been replaced from a specific
-  positive value (128) to `#"t'1`.
+  positive value (128) to `#"t'1`.  
+  It also contains CommonCCode, a file that stores the list of 
+  definition of the generated files that can be used to regenerate the
+  original C code files.
 * `ocaml-generator`: The Ocaml code of the previous Flight Plan generator of
 Paparazzi. This code has been extracted from the whole Paparazzi project
 and slightly modified for testing purpose (see
@@ -141,21 +145,19 @@ Currently, the generator as some limitations and known issues:
   execution return an integer value, evaluated as a boolean (returned value
   are converted into 0 or 1 only).
 * The parameter `last_wp` is a string.
-* Exceptions and forbidden deroute in loops are ignored.
+* Exceptions and forbidden deroutes in loops will cause 
+  `invalid flight_plan given` exception and prevent the auto-pilot
+  from being generated.
 * If the next block is forbidden then the execution state does not change.
   In theory, a warning should be raised in this case.
 * If there is an exception but the block is forbidden, then no deroute will
   occur.
+  A warning during the auto-pilot generation will indicate if there are
+  exceptions and forbidden deroutes that can contradict each other.
 * The field `exec` must be an instruction.
 
 ## Future works
 
-* Add a verified parser in Coq using menhir.
-* Prove that the `on_enter` and `on_enter` are always executed when
-  entering or leaving a block.
-* Generate a new `common_flight_plan.c` file from the modified version of
-  `CommonFP.v`. The Coq file is used to verify the semantics preservation theorem.
-* Add a warning for the exceptions with deroute that can be forbidden.
 * Prove that the errors detection always work for forbidden deroute.
 * Reduce the amount of modifications in the preprocessing:
   * Verify that the transformation of the `for` loop into a `while` loop is

docs/coq-descr-files.md

@@ -71,7 +71,7 @@ proof. The sources are divided into different subfolders:
     `pre_call_block`, `post_call_block` and `forbidden_deroute`.
 
 - `verification`: Contains the proof for the verification of the
-  semantics preservation.
+  semantics preservation and other generator properties.
   - `MatchFPwFPE.v`: Definition of matching relation between FP and
     FPE environment.
   - `MatchFPSwFPC.v`: Definition of the matching relation between FPS
@@ -79,6 +79,8 @@ proof. The sources are divided into different subfolders:
   - `ClightLemmas.v`: Lemmas about Clight properties.
   - `GeneratorProperties.v`: Properties about the generator needed for the
     verification.
+  - `FPSProp.v`: Properties about the generated code, proven on the FPS
+    semantics.
   - `CommonFPDefinition.v`: Contains definitions of functions and lemmas
     referring to the CommonFP file generated from the common C code.
   - `CommonFPSimplified.v`: Contains a simplified version of CommonFP (all
@@ -100,5 +102,15 @@ proof. The sources are divided into different subfolders:
   - `VerifFPToFPC.v`: File regrouping all the proof to verify the general
     bisimulation theorem between FP and Clight semantics.
 
+- `parser`: Contains the files used to generate the XML to FPP parser used in the frontend of the VFPG.
+  - `FlightPlanParsed.v`: Definition of the Flight Plan Parsed coq
+  structure that will store the result of the parsing.
+  - `FPPUtils.v`: Definitions of functions used to manipulate FPP.
+  - `CoqLexer.v`: Definition of the lexer used before the parser.
+  - `Parser.vy`: Grammar specification of a flight plan stored as a
+  XML file. It is given to Menhir to generate a verified parser in coq.
+  - `Importer.v`: Definition of the general parser function, taking a 
+  string and generating a FPP (or a procedure structure)
+
 Finally, the file `extraction.v` is the configuration file for the
 extraction of the Coq to Caml code.