Make minor modifications and generate code for loops

9 files changed, 213 insertions, 26 deletions

diff --git a/Makefile b/Makefile
index 797c8861..19ba0b6f 100644
--- a/Makefile
+++ b/Makefile
@@ -89,7 +89,8 @@ tests: trans-no_nested_borrows trans-paper \
 	trans-hashmap trans-hashmap_main \
 	trans-external trans-constants \
 	transp-polonius_list transp-betree_main \
-	test-transp-betree_main
+	test-transp-betree_main \
+	trans-loops
 
 # Verify the F* files generated by the translation
 .PHONY: verify
@@ -117,6 +118,11 @@ trans-no_nested_borrows trans-paper: \
 trans-no_nested_borrows trans-paper: SUBDIR:=misc
 tfstar-no_nested_borrows tfstar-paper:
 
+trans-loops: OPTIONS += -no-state
+trans-loops: SUBDIR := misc
+tfstar-loops: OPTIONS += -decreases-clauses -template-clauses
+tcoq-loops: OPTIONS += -use-fuel -no-split-files
+
 trans-hashmap: OPTIONS += -no-state
 trans-hashmap: SUBDIR:=hashmap
 tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
diff --git a/README.md b/README.md
index 3e711888..372d2f8a 100644
--- a/README.md
+++ b/README.md
@@ -45,7 +45,8 @@ We use **OCaml 4.13.1**: `opam switch create 4.13.1+options`
 The dependencies can then be installed with the following command:
 
 ```
-opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc unionFind
+opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc \
+  unionFind ocamlgraph
 ```
 
 Moreover, Aeneas requires the Charon ML library, defined in the
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index f870659a..3d2e84ad 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -11,6 +11,34 @@ module PrePasses = Aeneas.PrePasses
 module Translate = Aeneas.Translate
 open Aeneas.Config
 
+(** The local logger *)
+let log = main_log
+
+let _ =
+  (* Set up the logging - for now we use default values - TODO: use the
+   * command-line arguments *)
+  (* By setting a level for the main_logger_handler, we filter everything *)
+  Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
+  main_log#set_level EL.Info;
+  llbc_of_json_logger#set_level EL.Info;
+  pre_passes_log#set_level EL.Info;
+  interpreter_log#set_level EL.Info;
+  statements_log#set_level EL.Info;
+  loops_log#set_level EL.Info;
+  paths_log#set_level EL.Info;
+  expressions_log#set_level EL.Info;
+  expansion_log#set_level EL.Info;
+  projectors_log#set_level EL.Info;
+  borrows_log#set_level EL.Info;
+  invariants_log#set_level EL.Info;
+  pure_utils_log#set_level EL.Info;
+  symbolic_to_pure_log#set_level EL.Info;
+  pure_micro_passes_log#set_level EL.Info;
+  pure_to_extract_log#set_level EL.Info;
+  translate_log#set_level EL.Info;
+  scc_log#set_level EL.Info;
+  reorder_decls_log#set_level EL.Info
+
 (* This is necessary to have a backtrace when raising exceptions - for some
  * reason, the -g option doesn't work.
  * TODO: run with OCAMLRUNPARAM=b=1? *)
@@ -139,30 +167,6 @@ let () =
     if !dest_dir = "" then Filename.dirname filename else !dest_dir
   in
 
-  (* Set up the logging - for now we use default values - TODO: use the
-   * command-line arguments *)
-  (* By setting a level for the main_logger_handler, we filter everything *)
-  Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
-  let level = EL.Info in
-  main_log#set_level level;
-  llbc_of_json_logger#set_level level;
-  pre_passes_log#set_level level;
-  interpreter_log#set_level level;
-  statements_log#set_level level;
-  loops_log#set_level level;
-  paths_log#set_level level;
-  expressions_log#set_level level;
-  expansion_log#set_level level;
-  projectors_log#set_level level;
-  borrows_log#set_level level;
-  invariants_log#set_level level;
-  pure_utils_log#set_level level;
-  symbolic_to_pure_log#set_level level;
-  pure_micro_passes_log#set_level level;
-  pure_to_extract_log#set_level level;
-  translate_log#set_level level;
-  let log = main_log in
-
   (* Load the module *)
   let json = Yojson.Basic.from_file filename in
   match crate_of_json json with
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
new file mode 100644
index 00000000..48de76c2
--- /dev/null
+++ b/tests/coq/misc/Loops.v
@@ -0,0 +1,72 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [loops] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Module Loops.
+
+(** [loops::List] *)
+Inductive List_t (T : Type) :=
+| ListCons : T -> List_t T -> List_t T
+| ListNil : List_t T
+.
+
+Arguments ListCons {T} _ _.
+Arguments ListNil {T}.
+
+(** [loops::list_nth_mut_loop] *)
+Fixpoint list_nth_mut_loop_loop0_fwd
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons x tl =>
+      if i s= 0%u32
+      then Return x
+      else (
+        i0 <- u32_sub i 1%u32;
+        t <- list_nth_mut_loop_loop0_fwd T n0 tl i0;
+        Return t)
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_mut_loop] *)
+Definition list_nth_mut_loop_fwd
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
+  t <- list_nth_mut_loop_loop0_fwd T n ls i; Return t
+.
+
+(** [loops::list_nth_mut_loop] *)
+Fixpoint list_nth_mut_loop_loop0_back
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
+  result (List_t T)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match ls with
+    | ListCons x tl =>
+      if i s= 0%u32
+      then Return (ListCons ret tl)
+      else (
+        i0 <- u32_sub i 1%u32;
+        l <- list_nth_mut_loop_loop0_back T n0 tl i0 ret;
+        Return (ListCons x l))
+    | ListNil => Fail_ Failure
+    end
+  end
+.
+
+(** [loops::list_nth_mut_loop] *)
+Definition list_nth_mut_loop_back
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
+  result (List_t T)
+  :=
+  l <- list_nth_mut_loop_loop0_back T n ls i ret; Return l
+.
+
+End Loops .
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index c9ee0ff6..db6c2742 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -3,6 +3,7 @@
 -arg -w
 -arg all
 
+Loops.v
 Primitives.v
 External_Funs.v
 Constants.v
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
new file mode 100644
index 00000000..a898e9fb
--- /dev/null
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -0,0 +1,13 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [loops]: templates for the decreases clauses *)
+module Loops.Clauses.Template
+open Primitives
+open Loops.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [loops::list_nth_mut_loop]: decreases clause *)
+unfold
+let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
+  admit ()
+
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
new file mode 100644
index 00000000..e09eda9a
--- /dev/null
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -0,0 +1,12 @@
+(** [loops]: templates for the decreases clauses *)
+module Loops.Clauses
+open Primitives
+open Loops.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [loops::list_nth_mut_loop]: decreases clause *)
+unfold
+let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
+  i
+
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
new file mode 100644
index 00000000..f5339339
--- /dev/null
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -0,0 +1,66 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [loops]: function definitions *)
+module Loops.Funs
+open Primitives
+include Loops.Types
+include Loops.Clauses
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [loops::list_nth_mut_loop] *)
+let rec list_nth_mut_loop_loop0_fwd
+  (t : Type0) (ls : list_t t) (i : u32) :
+  Tot (result t) (decreases (list_nth_mut_loop_decreases t ls i))
+  =
+  begin match ls with
+  | ListCons x tl ->
+    if i = 0
+    then Return x
+    else
+      begin match u32_sub i 1 with
+      | Fail e -> Fail e
+      | Return i0 ->
+        begin match list_nth_mut_loop_loop0_fwd t tl i0 with
+        | Fail e -> Fail e
+        | Return x0 -> Return x0
+        end
+      end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop] *)
+let list_nth_mut_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t =
+  begin match list_nth_mut_loop_loop0_fwd t ls i with
+  | Fail e -> Fail e
+  | Return x -> Return x
+  end
+
+(** [loops::list_nth_mut_loop] *)
+let rec list_nth_mut_loop_loop0_back
+  (t : Type0) (ls : list_t t) (i : u32) (ret : t) :
+  Tot (result (list_t t)) (decreases (list_nth_mut_loop_decreases t ls i))
+  =
+  begin match ls with
+  | ListCons x tl ->
+    if i = 0
+    then Return (ListCons ret tl)
+    else
+      begin match u32_sub i 1 with
+      | Fail e -> Fail e
+      | Return i0 ->
+        begin match list_nth_mut_loop_loop0_back t tl i0 ret with
+        | Fail e -> Fail e
+        | Return l -> Return (ListCons x l)
+        end
+      end
+  | ListNil -> Fail Failure
+  end
+
+(** [loops::list_nth_mut_loop] *)
+let list_nth_mut_loop_back
+  (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) =
+  begin match list_nth_mut_loop_loop0_back t ls i ret with
+  | Fail e -> Fail e
+  | Return l -> Return l
+  end
+
diff --git a/tests/fstar/misc/Loops.Types.fst b/tests/fstar/misc/Loops.Types.fst
new file mode 100644
index 00000000..2e032fe7
--- /dev/null
+++ b/tests/fstar/misc/Loops.Types.fst
@@ -0,0 +1,12 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [loops]: type definitions *)
+module Loops.Types
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [loops::List] *)
+type list_t (t : Type0) =
+| ListCons : t -> list_t t -> list_t t
+| ListNil : list_t t
+