63 files changed, 18 insertions, 233 deletions
diff --git a/.gitignore b/.gitignore
index 1f9bd6a1..489b6f1c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -29,7 +29,7 @@ setup.log
 _opam/
 
 # Rust working directory
-rust-tests/target/
+rust-scripts/target/
 
 # F*
 .depend
diff --git a/Makefile b/Makefile
index eb09d1a0..4779bd22 100644
--- a/Makefile
+++ b/Makefile
@@ -14,7 +14,7 @@ CHARON_TESTS_DIR =
 CHARON_OPTIONS =
 CHARON_TESTS_SRC =
 
-AENEAS_DRIVER = src/driver.exe
+AENEAS_DRIVER = driver.exe
 
 # The user can specify additional translation options for Aeneas:
 OPTIONS ?=
@@ -35,11 +35,15 @@ build: build-driver build-lib doc
 
 .PHONY: build-driver
 build-driver:
-	dune build $(AENEAS_DRIVER)
+	cd compiler && dune build $(AENEAS_DRIVER)
 
 .PHONY: build-lib
 build-lib:
-	dune build src/aeneas.cmxs
+	cd compiler && dune build aeneas.cmxs
+
+.PHONY: doc
+doc:
+	cd compiler && dune build @doc
 
 # Test the project by translating test files to F*
 .PHONY: tests
@@ -100,11 +104,7 @@ trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc
 trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc
 
 trans-polonius-%: gen-llbc-polonius-%
-	dune exec -- $(AENEAS_DRIVER) $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
+	cd compiler && dune exec -- ./$(AENEAS_DRIVER) ../$(CHARON_TESTS_DIR)/$*.llbc -dest ../$(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
 
 trans-%: gen-llbc-%
-	dune exec -- $(AENEAS_DRIVER) $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
-
-.PHONY: doc
-doc:
-	dune build @doc
+	cd compiler && dune exec -- ./$(AENEAS_DRIVER) ../$(CHARON_TESTS_DIR)/$*.llbc -dest ../$(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
diff --git a/TODO.md b/TODO.md
deleted file mode 100644
index 39a16cdd..00000000
--- a/TODO.md
+++ /dev/null
@@ -1,213 +0,0 @@
-# TODO
-
-0. Priority:
-  * update treatment of matches
-  * remove prepass
-  * update pure expressions
-  * update control-flow reconstruction (Charon)
-
-0. Improve treatments of error and state error monads. In particular, introduce
-   `return` and `fail`, and remove `Return` and `Fail`.
-
-0. replace all the `failwith` with `raise (Failure ...)`: in CPS, it messes
-   up with provenance tracking
-
-0. In SymbolicToPure we do a few simplifications on types and values (simplification
-   of box type, removal of tuples which contain exactly one field - some fields
-   may have been filtered for the backward functions...): there are already a
-   few sanity checks, but we may to add more of them, which would type check
-   entire expressions for instance.
-
-0. merge the "read determinant" and the "switch" occurrences to "match"
-
-0. reaggregate the ADTs
-
-0. when going from symbolic to pure, remove the useless tuples (as some fields
-   might be erased).
-
-0. Update the high-level comments, in particular in Values.ml
-
-0. Rename Pure -> PureAst
-
-0. For variables pretty names: we could try to use the meta places used for the
-   forward function input vars to compute pretty names for the backward functions
-   output vars.
-
-0. sanity checks in symbolic to pure!
-
-0. update the end borrows internal to abstractions to not introduce a Bottom
-
-0. remove AConcrete from avalue
-
-0. remove ABottom from avalue
-
-0. micro-passes for pure:
-   - remove unused variables
-   - remove useless function calls:
-     - calls which don't introduce values *if* they are followed by associated
-       backward calls (because they may panic!)
-     - calls which don't take inputs (can happen with backward functions - for
-       instance, if a rust function only returns shared borrows)
-   - monadic lets to matches
-   - no tuple deconstruction on returned monadic values (introduce intermediate
-     variables to deconstruct in two times)
-   - matching on values (ex.: `let Cons hd tl = ls in` ~~>
-     `match ls with | Nil -> Panic | Cons hd tl -> ...`)
-
-1. reorder the branches of matches
-
-1. stateful maps/sets modules (hashtbl?)
-
-1. Check the occurrence of visitors like visit_AEndedMutLoan: the parameters are
-   sometimes inverted!
-
-2. check types are not "infinite"
-
-3. in MIR, erased regions are completely erased (no list of erased regions...):
-  update functions like `ty_has_regions` (and rename to `ty_has_borrows`),
-  `erase_regions`
-
-4. check that no borrow_overwrites upon ending abstractions
-
-5. add a check in function inputs: ok to take as parameters symbolic values with
-  borrow parameters *if* they come from the "input abstractions".
-  In order to do this, add a symbolic value kind (would make things easier than
-  adding ad-hoc lookups...): `FunRet`, `FunGivenBack`, `SynthInput`, `SynthGivenBack`
-  Rk.: pay attention: we can't give borrows of borrows to functions, but borrows
-  are ok.
-
-6. add `mvalue` (meta values) stored in abstractions when ending loans
-
-8. The following doesn't work (if we don't expand the symbolic values):
-  ```
-  fn f1<'c, T>(p : (&'c mut T, &'c mut T)) -> (&'c mut T, &'c mut T)
-
-  fn f2<'a, 'b, T>(p: (&'a mut T, &'b mut T)) -> (&'a mut T, &'b mut T)
-
-  let p1 = f1<'c>(p0);
-  let p2 = f2<'a, 'b>(p1);
-  ```
-  (end borrows)
-  I think we should change the proj_loans to:
-  `AProjLoans of symbolic_value * (mvalue * aproj) list`
-  (to accumulate the given back values)
-  Then, once we collected all the borrows, we would convert it to:
-  `AEndedProjLoans of (mvalue * aproj) list`
-  If the list is empty, it means the value was not modified.
-
-9. The way we currently give back symbolic values to symbolic values (inside
-   abstractions) is wrong.
-   We get things like :
-   `AProjLoans (s0 <: &'a mut T) [AProjBorrows (s1 <: &'a mut T)]`
-   while in the case of `s1` we should ignore the outer borrow (what we give
-   back actually has type `T`...)
-  
-10. Write "bodies" for the assumed functions.
-
-* write a function to check that the code we are about to synthesize is in the proper
-  subset. In particular:
-  * borrow overwrites
-  * type parameters instantiation
-  * uniform polymorphism
-  Also, write nice debug messages which refer to the original code in case
-  something fails.
-* write an interesting example to study with Jonathan
-
-* add option for: `allow_borrow_overwrites_on_input_values`
-  (rather: `will_overwrite_input_borrows`)
-  (but always disallow borrow overwrites on returned values)
-  at the level of abstractions (not at the level of loans!)
-
-* invariant: if there is a `proj_loans rset1 (s:rty)` where `s` contains mutable
-  borrows, then:
-  * either there is exactly one `s` in the current context
-  * or there is exactly one `proj_borrows rset2 (s:rty<:rty')` which intersects
-    the `proj_loans ...`
-  However, one `proj_borrows s` may intersect several `proj_loans` (in which
-  case we will need to split the value given back - for now: disallow this
-  behaviour?).
-
-* remove the rule which says that we can end a borrow under an abstraction if
-  the corresponding loan is in the same abstraction.
-  Actually: update the rule, rather.
-
-* update end_borrow_get_borrow to keep track of the ignored borrows/loans as
-  outer borrows, and track the ids of the ignored shared loans?
-  or: make sure there are no parent abstractions when ending inner loans in
-  abstractions.
-
-* `ended_proj_loans` (with ghost value)
-
-* make the projected shared borrows more structured? I don't think that's necessary
-
-* add a `allow_borrow_overwrites` in the loan projectors.
-
-* During printing, contexts are often big, with many variables containing "bottom".
-  Some variables also actually never get assigned, especially when they are used
-  for auxiliary assignments which don't exist anymore (because they were merged
-  with other operations - for arithmetic operations, for instance).
-  Maybe we should register which variable has been assigned at least once, and
-  print only those (thus skipping a big part of the environment for some time).
-
-* Some variables have the same name. It might be good to also print their id
-  to disambiguate?
-
-* it would be good to find a "core", which implements the rules (like
-  "end_borrow") and on top of which we build more complex functions which
-  chose in which order to apply the rules, etc. This way we would make very
-  explicit where we need to insert sanity checks, what the preconditions are,
-  where invariants might be broken, etc.
-
-* intensively test with PLT-redex
-
-* remove the config parameters when they are useless
-
-# DONE
-
-* update the assignment to move the destination value (which will be overriden)
-  to a dummy variable, and end all the outer borrows.
-  Also update pop_frame.
-
-* Check what happens when symbolic borrows are not expanded (when looking for
-  borrows/abstractions to end).
-
-* Detect loops in end_borrow/end_abstraction
-
-* recheck give_back_symbolic_value (use regions!)
-
-* expand symbolic values which are primitively copyable upon using them as
-  function arguments or putting them in the return value, in order to deduplicate
-  those values.
-  Completion: we expand those values only upon copying them (that's enough).
-
-* invariant: if a symbolic value is present multiple times in the concrete environment,
-  it means it is primitively copyable
-
-* update the printing of mut_borrows and mut_loans ([s@0 <: ...]) and (s@0)
-
-* add a switch to allow general symbolic values (containing references, etc.)
-  or not.
-
-* split `apply_proj_borrows` into two:
-  * `apply_proj_borrows_on_input_values` : ... -> value -> rty -> avalue
-  * `apply_proj_borrows_on_given_back_values` : ... -> value -> avalue -> avalue
-  Actually: didn't do it: bad idea.
-
-* Reduce projectors to `_` (ignored) when there are no region intersections
-
-* Add a `Collections.ml` file, with `Map` and `Set`
-
-* improve the use of [comp] for composition of functions with continuations
-
-* derive [ord] for types
-
-* compute the region constraints for the type definitions
-
-* set of types with mutable borrows (what to do when type variables appear under
-  shared borrows?), nested borrows...
-  necessary to know what to return.
-
-* fix the static regions (with projectors)
-  Before that, introduce a sanity check to make sure we don't use static regions.
-
-* add a meta-value in shared borrows to carry the shared value
diff --git a/src/.ocamlformat b/compiler/.ocamlformat
index b0ae150e..b0ae150e 100644
--- a/src/.ocamlformat
+++ b/compiler/.ocamlformat
diff --git a/src/Assumed.ml b/compiler/Assumed.ml
index cb089c08..cb089c08 100644
--- a/src/Assumed.ml
+++ b/compiler/Assumed.ml
diff --git a/src/Collections.ml b/compiler/Collections.ml
index 0933b3e4..0933b3e4 100644
--- a/src/Collections.ml
+++ b/compiler/Collections.ml
diff --git a/src/ConstStrings.ml b/compiler/ConstStrings.ml
index ae169a2e..ae169a2e 100644
--- a/src/ConstStrings.ml
+++ b/compiler/ConstStrings.ml
diff --git a/src/Contexts.ml b/compiler/Contexts.ml
index 510976f4..510976f4 100644
--- a/src/Contexts.ml
+++ b/compiler/Contexts.ml
diff --git a/src/Cps.ml b/compiler/Cps.ml
index c2c0363b..c2c0363b 100644
--- a/src/Cps.ml
+++ b/compiler/Cps.ml
diff --git a/src/Crates.ml b/compiler/Crates.ml
index 844afb94..844afb94 100644
--- a/src/Crates.ml
+++ b/compiler/Crates.ml
diff --git a/src/Errors.ml b/compiler/Errors.ml
index 31a53cf4..31a53cf4 100644
--- a/src/Errors.ml
+++ b/compiler/Errors.ml
diff --git a/src/Expressions.ml b/compiler/Expressions.ml
index e2eaf1e7..e2eaf1e7 100644
--- a/src/Expressions.ml
+++ b/compiler/Expressions.ml
diff --git a/src/ExpressionsUtils.ml b/compiler/ExpressionsUtils.ml
index c3ccfb15..c3ccfb15 100644
--- a/src/ExpressionsUtils.ml
+++ b/compiler/ExpressionsUtils.ml
diff --git a/src/ExtractToFStar.ml b/compiler/ExtractToFStar.ml
index 5d212941..5d212941 100644
--- a/src/ExtractToFStar.ml
+++ b/compiler/ExtractToFStar.ml
diff --git a/src/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 248ad8b3..248ad8b3 100644
--- a/src/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
diff --git a/src/Identifiers.ml b/compiler/Identifiers.ml
index b022b18d..b022b18d 100644
--- a/src/Identifiers.ml
+++ b/compiler/Identifiers.ml
diff --git a/src/Interpreter.ml b/compiler/Interpreter.ml
index 7f51c5b9..7f51c5b9 100644
--- a/src/Interpreter.ml
+++ b/compiler/Interpreter.ml
diff --git a/src/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 30c3b221..30c3b221 100644
--- a/src/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
diff --git a/src/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index a5501712..a5501712 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
diff --git a/src/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 0ca34b43..0ca34b43 100644
--- a/src/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
diff --git a/src/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 62d9b80b..62d9b80b 100644
--- a/src/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
diff --git a/src/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index d54a046e..d54a046e 100644
--- a/src/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
diff --git a/src/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 064b8969..064b8969 100644
--- a/src/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
diff --git a/src/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 4e61e683..4e61e683 100644
--- a/src/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
diff --git a/src/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index e6033e9e..e6033e9e 100644
--- a/src/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
diff --git a/src/Invariants.ml b/compiler/Invariants.ml
index 4a3364a6..4a3364a6 100644
--- a/src/Invariants.ml
+++ b/compiler/Invariants.ml
diff --git a/src/LlbcAst.ml b/compiler/LlbcAst.ml
index 1b08f1ea..1b08f1ea 100644
--- a/src/LlbcAst.ml
+++ b/compiler/LlbcAst.ml
diff --git a/src/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index 46711d0a..46711d0a 100644
--- a/src/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
diff --git a/src/LlbcOfJson.ml b/compiler/LlbcOfJson.ml
index 79c9b756..79c9b756 100644
--- a/src/LlbcOfJson.ml
+++ b/compiler/LlbcOfJson.ml
diff --git a/src/Logging.ml b/compiler/Logging.ml
index e83f25f8..e83f25f8 100644
--- a/src/Logging.ml
+++ b/compiler/Logging.ml
diff --git a/src/Meta.ml b/compiler/Meta.ml
index f0e4ca04..f0e4ca04 100644
--- a/src/Meta.ml
+++ b/compiler/Meta.ml
diff --git a/src/Names.ml b/compiler/Names.ml
index a27db161..a27db161 100644
--- a/src/Names.ml
+++ b/compiler/Names.ml
diff --git a/src/OfJsonBasic.ml b/compiler/OfJsonBasic.ml
index 07daf03d..07daf03d 100644
--- a/src/OfJsonBasic.ml
+++ b/compiler/OfJsonBasic.ml
diff --git a/src/PrePasses.ml b/compiler/PrePasses.ml
index a09ae476..a09ae476 100644
--- a/src/PrePasses.ml
+++ b/compiler/PrePasses.ml
diff --git a/src/Print.ml b/compiler/Print.ml
index 03cab6ee..8f52b291 100644
--- a/src/Print.ml
+++ b/compiler/Print.ml
@@ -951,7 +951,7 @@ module LlbcAst = struct
         indent ^ "set_discriminant(" ^ place_to_string fmt p ^ ", "
         ^ T.VariantId.to_string variant_id
         ^ ")"
-    | A.Drop p -> indent ^ "drop(" ^ place_to_string fmt p ^ ")"
+    | A.Drop p -> indent ^ "drop " ^ place_to_string fmt p
     | A.Assert a ->
         let cond = operand_to_string fmt a.A.cond in
         if a.A.expected then indent ^ "assert(" ^ cond ^ ")"
diff --git a/src/PrintPure.ml b/compiler/PrintPure.ml
index a9e42f6c..a9e42f6c 100644
--- a/src/PrintPure.ml
+++ b/compiler/PrintPure.ml
diff --git a/src/Pure.ml b/compiler/Pure.ml
index 77265f75..77265f75 100644
--- a/src/Pure.ml
+++ b/compiler/Pure.ml
diff --git a/src/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 3edae38a..3edae38a 100644
--- a/src/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
diff --git a/src/PureToExtract.ml b/compiler/PureToExtract.ml
index 77c3afd4..77c3afd4 100644
--- a/src/PureToExtract.ml
+++ b/compiler/PureToExtract.ml
diff --git a/src/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index caad8a58..caad8a58 100644
--- a/src/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
diff --git a/src/PureUtils.ml b/compiler/PureUtils.ml
index 39f3d76a..39f3d76a 100644
--- a/src/PureUtils.ml
+++ b/compiler/PureUtils.ml
diff --git a/src/Scalars.ml b/compiler/Scalars.ml
index 03ca506c..03ca506c 100644
--- a/src/Scalars.ml
+++ b/compiler/Scalars.ml
diff --git a/src/StringUtils.ml b/compiler/StringUtils.ml
index 0fd46136..0fd46136 100644
--- a/src/StringUtils.ml
+++ b/compiler/StringUtils.ml
diff --git a/src/Substitute.ml b/compiler/Substitute.ml
index 5e5858de..5e5858de 100644
--- a/src/Substitute.ml
+++ b/compiler/Substitute.ml
diff --git a/src/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 604a7948..604a7948 100644
--- a/src/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
diff --git a/src/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index de4fb4c1..de4fb4c1 100644
--- a/src/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
diff --git a/src/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index a2256bdd..a2256bdd 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
diff --git a/src/Translate.ml b/compiler/Translate.ml
index 8f3b94c4..8f3b94c4 100644
--- a/src/Translate.ml
+++ b/compiler/Translate.ml
diff --git a/src/TranslateCore.ml b/compiler/TranslateCore.ml
index a658147d..a658147d 100644
--- a/src/TranslateCore.ml
+++ b/compiler/TranslateCore.ml
diff --git a/src/Types.ml b/compiler/Types.ml
index 326ef76f..326ef76f 100644
--- a/src/Types.ml
+++ b/compiler/Types.ml
diff --git a/src/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 60ce5149..60ce5149 100644
--- a/src/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
diff --git a/src/TypesUtils.ml b/compiler/TypesUtils.ml
index 7531dd8b..7531dd8b 100644
--- a/src/TypesUtils.ml
+++ b/compiler/TypesUtils.ml
diff --git a/src/Utils.ml b/compiler/Utils.ml
index a285e869..a285e869 100644
--- a/src/Utils.ml
+++ b/compiler/Utils.ml
diff --git a/src/Values.ml b/compiler/Values.ml
index e404f40d..e404f40d 100644
--- a/src/Values.ml
+++ b/compiler/Values.ml
diff --git a/src/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 72d7abe0..72d7abe0 100644
--- a/src/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
diff --git a/aeneas.opam b/compiler/aeneas.opam
index 4048f9a0..4048f9a0 100644
--- a/aeneas.opam
+++ b/compiler/aeneas.opam
diff --git a/src/driver.ml b/compiler/driver.ml
index ae9d238a..ae9d238a 100644
--- a/src/driver.ml
+++ b/compiler/driver.ml
diff --git a/src/dune b/compiler/dune
index e8b53fc5..e8b53fc5 100644
--- a/src/dune
+++ b/compiler/dune
diff --git a/dune-project b/compiler/dune-project
index f8b418f2..f8b418f2 100644
--- a/dune-project
+++ b/compiler/dune-project
diff --git a/fstar/Primitives.fst b/compiler/fstar/Primitives.fst
index b44fe9d1..b44fe9d1 100644
--- a/fstar/Primitives.fst
+++ b/compiler/fstar/Primitives.fst
diff --git a/rust-scripts/Cargo.toml b/rust-scripts/Cargo.toml
new file mode 100644
index 00000000..31ef5be0
--- /dev/null
+++ b/rust-scripts/Cargo.toml
@@ -0,0 +1,7 @@
+[package]
+name = "rust-tests"
+version = "0.1.0"
+authors = ["Son Ho <hosonmarc@gmail.com>"]
+edition = "2018"
+
+[dependencies]
+\ No newline at end of file
diff --git a/rust-tests/src/main.rs b/rust-scripts/src/main.rs
index 125b0d76..125b0d76 100644
--- a/rust-tests/src/main.rs
+++ b/rust-scripts/src/main.rs
diff --git a/rust-tests/Cargo.toml b/rust-tests/Cargo.toml
deleted file mode 100644
index e384da1d..00000000
--- a/rust-tests/Cargo.toml
+++ /dev/null
@@ -1,9 +0,0 @@
-[package]
-name = "rust-tests"
-version = "0.1.0"
-authors = ["Son Ho <hosonmarc@gmail.com>"]
-edition = "2018"
-
-# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
-
-[dependencies]