diff options
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | README.md | 3 | ||||
| -rw-r--r-- | compiler/Driver.ml | 52 | ||||
| -rw-r--r-- | tests/coq/misc/Loops.v | 72 | ||||
| -rw-r--r-- | tests/coq/misc/_CoqProject | 1 | ||||
| -rw-r--r-- | tests/fstar/misc/Loops.Clauses.Template.fst | 13 | ||||
| -rw-r--r-- | tests/fstar/misc/Loops.Clauses.fst | 12 | ||||
| -rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 66 | ||||
| -rw-r--r-- | tests/fstar/misc/Loops.Types.fst | 12 |
9 files changed, 213 insertions, 26 deletions
@@ -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 @@ -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 + |