From 6b2884a5347eca1607d1c9aaf5c77af12e3170d3 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 14 Jun 2022 07:24:43 +0200 Subject: Update the README --- README.md | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/README.md b/README.md index f31ae3b0..1a8fb901 100644 --- a/README.md +++ b/README.md @@ -11,10 +11,10 @@ Wall in Pompei, digital image from Michael Lahanis. # Aeneas -Aeneas is a compiler from LLBC, a language inspired by Rust's MIR, to pure lambda calculus. -It is intended to be used in combination with [Charon](https://github.com/Kachoc/charon), -which compiles Rust programs to LLBC, to allow the verification of Rust programs in -proof assistants. It currently has a backend for the [F\*](https://www.fstar-lang.org) +Aeneas is a verification toolchain for Rust programs. It relies on a translation from Rusts's MIR +internal language to a pure lamdba calculus. It is intended to be used in combination with +[Charon](https://github.com/Kachoc/charon), which compiles Rust programs to an intermediate +representation called LLBC. It currently has a backend for the [F\*](https://www.fstar-lang.org) theorem prover, and we intend to add backends for other provers such as [Coq](https://coq.inria.fr/), [HOL4](https://hol-theorem-prover.org/) or [LEAN](https://leanprover.github.io/). @@ -73,12 +73,10 @@ We have the following limitations, that we plan to address one by one: issue. We intend to quickly address the issue for types (i.e., allow `Option<&mut T>`), and later address it for functions (i.e., allow `f<&mut T>` - we consider this to be less urgent). -- **no nested borrows in function signatures**. See the paper for a detailed - discussion. We might allow nested borrows while forbiding what we call - "borrow overwrites" (see the paper) as a first step towards supporting this feature. +- **no nested borrows in function signatures**: ongoing work. - **no interior mutability**: long-term effort. Interior mutability introduces - true aliasing: we will probably have to combine our pure lambda calculus - with separation logic to address this. + true aliasing: we will probably have to use a low-level memory model to address + this issue. Note that interior mutability is mostly anecdotal in sequential execution, but necessary for concurrent execution (it is exploited by the synchronisation primitives). -- cgit v1.2.3 From ca29ee86221db6c115f498a1f8f6315325196d24 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 14 Jun 2022 07:25:45 +0200 Subject: Update the README --- README.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 1a8fb901..c7b98b5e 100644 --- a/README.md +++ b/README.md @@ -77,8 +77,7 @@ We have the following limitations, that we plan to address one by one: - **no interior mutability**: long-term effort. Interior mutability introduces true aliasing: we will probably have to use a low-level memory model to address this issue. - Note that interior mutability is mostly anecdotal in sequential execution, - but necessary for concurrent execution (it is exploited by the synchronisation - primitives). + Note that interior mutability is truely necessary for concurrent execution (it + is exploited to implement the synchronisation primitives). - **no concurrent execution**: long-term effort. We plan to address coarse-grained parallelism as a long-term goal. -- cgit v1.2.3 From f51f4c5d883691ef73094a79b4316255191627b0 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 20 Jun 2022 06:02:53 +0200 Subject: Remove a comment --- tests/hashmap/Hashmap.Properties.fst | 189 ----------------------------------- 1 file changed, 189 deletions(-) diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst index 12c47d1f..21a46c73 100644 --- a/tests/hashmap/Hashmap.Properties.fst +++ b/tests/hashmap/Hashmap.Properties.fst @@ -11,195 +11,6 @@ open Hashmap.Funs let _align_fsti = () -/// Issues encountered with F*: -/// =========================== -/// -/// The proofs actually caused a lot more trouble than expected, because of the -/// below points. All those are problems I already encountered in the past, but: -/// -/// - the fact that I spent 9 months mostly focusing on Aeneas made me forget them -/// a bit -/// - they seem exacerbated by the fact that they really matter when doing -/// functional correctness proofs, while Aeneas allows me to focus on the -/// functional behaviour of my programs. -/// -/// As a simple example, when I implemented linked lists (with loops) in Low* -/// for Noise*, most of the work consisted in making the Low* proofs work -/// (which was painful). -/// -/// There was a bit of functional reasoning (for which I already encountered the -/// below issues), but it was pretty simple and shadowed by the memory management -/// part. In the current situation, as we got rid of the memory management annoyance, -/// we could move on to the more the complex hash maps where the functional correctness -/// proofs *actually* require some work, making extremely obvious the problems F* has -/// when dealing with this kind of proofs. -/// -/// Here, I would like to emphasize the fact that if hash maps *do* have interesting -/// functional properties to study, I don't believe those properties are *intrinsically* -/// complex. In particular, I am very eager to try to do the same proofs in Coq or -/// HOL4, which I believe are more suited to this kind of proofs, and see how things go. -/// I'm aware that those provers also suffer from drawbacks, but I believe those are -/// less severe than F* in the present case. -/// -/// The problems I encountered (once again, all this is well known): -/// -/// - we are blind when doing the proofs. After a very intensive use of F* I got -/// used to it meaning I *can* do proofs in F*, but it still takes me a tremendous -/// amout of energy to visualize the context in my head and, for instance, -/// properly instantiate the lemmas or insert the necessary assertions in the code. -/// I actually often write assertions that I assume just to *check* that those -/// assertions make the proofs pass and are thus indeed the ones I want to prove, -/// which is something very specific to working with F*. -/// -/// About the fact that we are blind: see [hash_map_try_resize_fwd_back_lem_refin] -/// -/// - the fact that we don't reason with tactics but with the SMT solver with an -/// "intrinsic" style of proofs makes it a bit awkward to reason about pure -/// functions in a modular manner, because every proof requires to basically -/// copy-paste the function we are studying. As a consequence, this file is -/// very verbose (look at the number of lines of code...). -/// -/// - F* is extremely bad at reasoning with quantifiers, which is made worse by -/// the fact we are blind when making proofs. This forced me to be extremely -/// careful about the way I wrote the specs/invariants (by writing "functional" -/// specs and invariants, mostly, so as not to manipulate quantifiers). -/// -/// In particular, I had to cut the proofs into many steps just for this reason, -/// while if I had been able to properly use quantifiers (I tried: in many -/// situations I manage to massage F* to make it work, but in the below proofs -/// it was horrific) I would have proven many results in one go. -/// -/// More specifically: the hash map has an invariant stating that all the keys -/// are pairwise disjoint. This invariant is extremely simple to write with -/// forall quantifiers and looks like the following: -/// `forall i j. i <> j ==> key_at i hm <> key_at j hm` -/// -/// If you can easily manipulate forall quantifiers, you can prove that the -/// invariant is maintained by, say, the insertion functions in one go. -/// -/// However here, because I couldn't make the quantification work (and I really -/// tried hard, because this is a very natural way of doing the proofs), I had -/// to resort to invariants written in terms of [pairwise_rel]. This is -/// extremely annoying, because then the process becomes: -/// - prove that the insertion, etc. functions refine some higher level functions -/// (that I have to introduce) -/// - prove that those higher level functions preserve the invariants -/// -/// All this results in a huge amount of intermediary lemmas and definitions... -/// Of course, I'm totally fine with introducing refinements steps when the -/// proofs are *actually* intrinsically complex, but here we are studying hash -/// maps, so come on!! -/// -/// - the abundance of intermediate definitions and lemmas causes a real problem -/// because we then have to remember them, find naming conventions (otherwise -/// it is a mess) and go look for them. All in all, it takes engineering time, -/// and it can quickly cause scaling issues... -/// -/// - F* doesn't encode closures properly, the result being that it is very -/// awkward to reason about functions like [map] or [find], because we have -/// to introduce auxiliary definitions for the parameters we give to those -/// functions (if we use anonymous lambda functions, we're screwed by the -/// encoding). -/// See all the definitions like [same_key], [binding_neq], etc. which cluter -/// the file and worsen the problem mentionned in the previous point. -/// -/// - we can't prove intermediate results which require a *recursive* proof -/// inside of other proofs, meaning that whenever we need such a result we need -/// to write an intermediate lemma, which is extremely cumbersome. -/// -/// What is extremely frustrating is that in most situations, those intermediate -/// lemmas are extremely simple to prove: they would simply need 2 or 3 tactic -/// calls in Coq or HOL4, and in F* the proof is reduced to a recursive call. -/// Isolating the lemma (i.e., writing its signature), however, takes some -/// non-negligible time, which is made worse by the fact that, once again, -/// we don't have proof contexts to stare at which would help figure out -/// how to write such lemmas. -/// -/// Simple example: see [for_all_binding_neq_find_lem]. This lemma states that: -/// "if a key is not in a map, then looking up this key returns None" (and those -/// properties are stated in two different styles, hence the need for a proof). -/// This lemma is used in *exactly* one place, and simply needs a recursive call. -/// Stating the lemma took a lot more time (and place) than proving it. -/// -/// - more generally, it can be difficult to figure out which intermediate results -/// to prove. In an interactive theorem prover based on tactics, it often happens -/// that we start proving the theorem we target, then get stuck on a proof obligation -/// for which we realize we need to prove an intermediate result. -/// -/// This process is a lot more difficult in F*, and I have to spend a lot of energy -/// figuring out what I *might* need in the future. While this is probably a good -/// habit, there are many situations where it is really a constraint: I'm often -/// reluctant before starting a new proof in F*, because I anticipate on this very -/// annoying loop: try to prove something, get an unknown assertion failed error, -/// insert a lot of assertions or think *really* deeply to figure out what might -/// have happened, etc. All this seems a lot more natural when working with tactics. -/// -/// Simple example: see [slots_t_inv_implies_slots_s_inv]. This lemma is super -/// simple and was probably not required (it is proven with `()`). But I often feel -/// forced to anticipate on problems, otherwise proofs become too painful. -/// -/// - the proofs often fail or succeed for extremely unpredictable reasons, and are -/// extremely hard to debug. -/// -/// 1. See the comments for [hash_map_move_elements_fwd_back_lem_refin], which -/// describe the various breakages I encountered, and the different attempts I -/// made to fix them. As explained in those comments, the frustrating part is that -/// the proof is a very simple refinement step: this is not the kind of place where -/// I expected to spend time. -/// -/// Also, now that I know why it was brittle in the first place, I don't understand -/// why it worked at some point. One big issue is that when trying to figure out -/// why F* (or rather Z3) fails (for instance when playing with Z3's parameters), we -/// are constantly shooting in the dark. -/// -/// 2. See [hash_map_is_assoc_list] and [hash_map_move_elements_fwd_back_lem]. -/// -/// In particular, [hash_map_move_elements_fwd_back_lem] was very painful, with -/// assertions directly given by some postconditions which failed for no reasons, -/// or "unknown assertion failed" which forced us to manually insert -/// the postconditions given by the lemmas we called (resulting in a verbose -/// proof)... -/// -/// 4. As usual, the unstable arithmetic proofs are a lot of fun. We have a few -/// of them because we prove that the table is never over-loaded (it resizes itself -/// in order to respect the max load factor). See [new_max_load_lem] for instance. -/// -/// Finally: remember (again) that we are in a pure setting. Imagine having to -/// deal with Low*/separation logic at the same time. -/// -/// - debugging a proof can be difficult, especially when Z3 simply answers with -/// "Unknown assertion failed". Rolling admits work reasonably well, though time -/// consuming, but they cause trouble when the failing proof obligation is in the -/// postcondition of the function: in this situation we need to copy-paste the -/// postcondition in order to be able to do the rolling admit. As we may need to -/// rename some variables, this implies copying the post, instantiating it (by hand), -/// checking that it is correct (by assuming it and making sure the proofs pass), -/// then doing the rolling admit, assertion by assertion. This is tedious and, -/// combined with F*'s answer time, very time consuming (and boring!). -/// -/// See [hash_map_insert_fwd_back_lem] for instance. -/// -/// As a sub-issue, I often encountered in my experience with F* the problem of -/// failing to prove the equality between two records, in which case F* just -/// tells you that Z3 was not able to prove the *whole* equality, but doesn't -/// give you information about the precise fields. In a prover with tactics -/// you immediately see which fields is problematic, because you get stuck with -/// a goal like: -/// ``` -/// Cons x y z == Cons x' y z -/// ``` -/// -/// In F* you have to manually expand the equality to a conjunction of field -/// equalities. See [hash_map_try_resize_fwd_back_lem_refin] for an illustration. -/// -/// - overall, there are many things we have to do to debug the failing proofs -/// which are very tedious, repetitive, manual and boring (which is kind of -/// ironic for computer scientists), are specific to F* and require *writing -/// a lot*. For instance, taking items from the above points: -/// - inserting assertions -/// - copy-pasting pre/postconditions to apply a rolling admit technique -/// - expanding a record equality to a conjunction of field equalities - /// The proofs: /// =========== /// -- cgit v1.2.3 From 4c3a164ed570ecfa721255519554911754913271 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 20 Jun 2022 06:21:57 +0200 Subject: Add makefiles to test the F* files --- Makefile | 13 +++++++---- tests/Makefile | 19 +++++++++++++++ tests/Makefile.template | 51 ++++++++++++++++++++++++++++++++++++++++ tests/betree/Makefile | 51 ++++++++++++++++++++++++++++++++++++++++ tests/hashmap/Makefile | 51 ++++++++++++++++++++++++++++++++++++++++ tests/hashmap_on_disk/Makefile | 51 ++++++++++++++++++++++++++++++++++++++++ tests/misc/Makefile | 53 ++++++++++++++++++++++++++++++++++++++++-- 7 files changed, 283 insertions(+), 6 deletions(-) create mode 100644 tests/Makefile create mode 100644 tests/Makefile.template create mode 100644 tests/betree/Makefile create mode 100644 tests/hashmap/Makefile create mode 100644 tests/hashmap_on_disk/Makefile diff --git a/Makefile b/Makefile index 1e62dfd5..58919a7b 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,4 @@ -all: build-test +all: build-test-verify CHARON_HOME = ../charon CHARON_EXEC = $(CHARON_HOME)/charon @@ -19,21 +19,26 @@ TRANS_OPTIONS := -test-trans-units $(OPTIONS) SUBDIR := # Build the project and test it -.PHONY: build-test -build-test: build test +.PHONY: build-test-verify +build-test-verify: build test verify # Build the project .PHONY: build build: dune build src/main.exe -# Test the project +# Test the project by translating test files to F* .PHONY: test test: build trans-no_nested_borrows trans-paper \ trans-hashmap trans-hashmap_main \ trans-external trans-nll-betree_nll \ trans-nll-betree_main +# Verify the translated F* files +.PHONY: verify +verify: build test + cd tests && make all + # Add specific options to some tests trans-no_nested_borrows trans-paper: \ TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses diff --git a/tests/Makefile b/tests/Makefile new file mode 100644 index 00000000..a9c170f7 --- /dev/null +++ b/tests/Makefile @@ -0,0 +1,19 @@ +ALL_DIRS ?= $(filter-out Makefile%, $(wildcard *)) + +VERIFY_DIRS = $(addprefix verif-,$(ALL_DIRS)) + +CLEAN_DIRS = $(addprefix clean-,$(ALL_DIRS)) + +.PHONY: all +all: $(VERIFY_DIRS) + +.PHONY: clean +clean: $(CLEAN_DIRS) + +.PHONY: verif-% +verif-%: + cd $* && make all + +.PHONY: clean-% +clean-%: + cd $* && make clean diff --git a/tests/Makefile.template b/tests/Makefile.template new file mode 100644 index 00000000..fed1a280 --- /dev/null +++ b/tests/Makefile.template @@ -0,0 +1,51 @@ +INCLUDE_DIRS = . + +FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) + +FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints + +FSTAR_OPTIONS = $(FSTAR_HINTS) \ + --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ + --warn_error '+241@247+285-274' \ + --cache_dir obj + +FSTAR_NO_FLAGS = fstar.exe + +FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) + +# The F* roots are used to compute the dependency graph, and generate the .depend file +FSTAR_ROOTS ?= $(wildcard *.fst *.fsti) + +# This is the right way to ensure the .depend file always gets re-built. +ifeq (,$(filter %-in,$(MAKECMDGOALS))) +ifndef NODEPEND +ifndef MAKE_RESTARTS +.depend: .FORCE + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ + --extract 'krml:*' \ + --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ + > $@ + +.PHONY: .FORCE +.FORCE: +endif +endif + +include .depend +endif + +# For the interactive mode +%.fst %.fsti: + $(FSTAR) $@ + +# Generete the .checked files in bash mode +%.checked: + $(FSTAR) $(FSTAR_FLAGS) $* && \ + touch -c $* + +# Build all the files +all: $(ALL_CHECKED_FILES) + +.PHONY: clean +clean: + rm -f obj/* diff --git a/tests/betree/Makefile b/tests/betree/Makefile new file mode 100644 index 00000000..fed1a280 --- /dev/null +++ b/tests/betree/Makefile @@ -0,0 +1,51 @@ +INCLUDE_DIRS = . + +FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) + +FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints + +FSTAR_OPTIONS = $(FSTAR_HINTS) \ + --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ + --warn_error '+241@247+285-274' \ + --cache_dir obj + +FSTAR_NO_FLAGS = fstar.exe + +FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) + +# The F* roots are used to compute the dependency graph, and generate the .depend file +FSTAR_ROOTS ?= $(wildcard *.fst *.fsti) + +# This is the right way to ensure the .depend file always gets re-built. +ifeq (,$(filter %-in,$(MAKECMDGOALS))) +ifndef NODEPEND +ifndef MAKE_RESTARTS +.depend: .FORCE + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ + --extract 'krml:*' \ + --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ + > $@ + +.PHONY: .FORCE +.FORCE: +endif +endif + +include .depend +endif + +# For the interactive mode +%.fst %.fsti: + $(FSTAR) $@ + +# Generete the .checked files in bash mode +%.checked: + $(FSTAR) $(FSTAR_FLAGS) $* && \ + touch -c $* + +# Build all the files +all: $(ALL_CHECKED_FILES) + +.PHONY: clean +clean: + rm -f obj/* diff --git a/tests/hashmap/Makefile b/tests/hashmap/Makefile new file mode 100644 index 00000000..fed1a280 --- /dev/null +++ b/tests/hashmap/Makefile @@ -0,0 +1,51 @@ +INCLUDE_DIRS = . + +FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) + +FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints + +FSTAR_OPTIONS = $(FSTAR_HINTS) \ + --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ + --warn_error '+241@247+285-274' \ + --cache_dir obj + +FSTAR_NO_FLAGS = fstar.exe + +FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) + +# The F* roots are used to compute the dependency graph, and generate the .depend file +FSTAR_ROOTS ?= $(wildcard *.fst *.fsti) + +# This is the right way to ensure the .depend file always gets re-built. +ifeq (,$(filter %-in,$(MAKECMDGOALS))) +ifndef NODEPEND +ifndef MAKE_RESTARTS +.depend: .FORCE + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ + --extract 'krml:*' \ + --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ + > $@ + +.PHONY: .FORCE +.FORCE: +endif +endif + +include .depend +endif + +# For the interactive mode +%.fst %.fsti: + $(FSTAR) $@ + +# Generete the .checked files in bash mode +%.checked: + $(FSTAR) $(FSTAR_FLAGS) $* && \ + touch -c $* + +# Build all the files +all: $(ALL_CHECKED_FILES) + +.PHONY: clean +clean: + rm -f obj/* diff --git a/tests/hashmap_on_disk/Makefile b/tests/hashmap_on_disk/Makefile new file mode 100644 index 00000000..fed1a280 --- /dev/null +++ b/tests/hashmap_on_disk/Makefile @@ -0,0 +1,51 @@ +INCLUDE_DIRS = . + +FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) + +FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints + +FSTAR_OPTIONS = $(FSTAR_HINTS) \ + --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ + --warn_error '+241@247+285-274' \ + --cache_dir obj + +FSTAR_NO_FLAGS = fstar.exe + +FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) + +# The F* roots are used to compute the dependency graph, and generate the .depend file +FSTAR_ROOTS ?= $(wildcard *.fst *.fsti) + +# This is the right way to ensure the .depend file always gets re-built. +ifeq (,$(filter %-in,$(MAKECMDGOALS))) +ifndef NODEPEND +ifndef MAKE_RESTARTS +.depend: .FORCE + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ + --extract 'krml:*' \ + --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ + > $@ + +.PHONY: .FORCE +.FORCE: +endif +endif + +include .depend +endif + +# For the interactive mode +%.fst %.fsti: + $(FSTAR) $@ + +# Generete the .checked files in bash mode +%.checked: + $(FSTAR) $(FSTAR_FLAGS) $* && \ + touch -c $* + +# Build all the files +all: $(ALL_CHECKED_FILES) + +.PHONY: clean +clean: + rm -f obj/* diff --git a/tests/misc/Makefile b/tests/misc/Makefile index 5153d201..fed1a280 100644 --- a/tests/misc/Makefile +++ b/tests/misc/Makefile @@ -1,2 +1,51 @@ -%.fst-in %.fsti-in: - @echo --include ../hashmap +INCLUDE_DIRS = . + +FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) + +FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints + +FSTAR_OPTIONS = $(FSTAR_HINTS) \ + --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ + --warn_error '+241@247+285-274' \ + --cache_dir obj + +FSTAR_NO_FLAGS = fstar.exe + +FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) + +# The F* roots are used to compute the dependency graph, and generate the .depend file +FSTAR_ROOTS ?= $(wildcard *.fst *.fsti) + +# This is the right way to ensure the .depend file always gets re-built. +ifeq (,$(filter %-in,$(MAKECMDGOALS))) +ifndef NODEPEND +ifndef MAKE_RESTARTS +.depend: .FORCE + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ + --extract 'krml:*' \ + --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ + > $@ + +.PHONY: .FORCE +.FORCE: +endif +endif + +include .depend +endif + +# For the interactive mode +%.fst %.fsti: + $(FSTAR) $@ + +# Generete the .checked files in bash mode +%.checked: + $(FSTAR) $(FSTAR_FLAGS) $* && \ + touch -c $* + +# Build all the files +all: $(ALL_CHECKED_FILES) + +.PHONY: clean +clean: + rm -f obj/* -- cgit v1.2.3 From 227869ddd73782834162c64a34f260b438f5cbae Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 20 Jun 2022 06:23:44 +0200 Subject: Make minor modifications --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 58919a7b..694dc964 100644 --- a/Makefile +++ b/Makefile @@ -18,7 +18,7 @@ OPTIONS ?= TRANS_OPTIONS := -test-trans-units $(OPTIONS) SUBDIR := -# Build the project and test it +# Build the project, test it and verify the generated files .PHONY: build-test-verify build-test-verify: build test verify @@ -34,7 +34,7 @@ test: build trans-no_nested_borrows trans-paper \ trans-external trans-nll-betree_nll \ trans-nll-betree_main -# Verify the translated F* files +# Verify the F* files generated by the translation .PHONY: verify verify: build test cd tests && make all -- cgit v1.2.3 From 3a930571516912714e3dcbc7ed1968228e593f99 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 20 Jun 2022 06:24:43 +0200 Subject: Update the .gitignore file --- .gitignore | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.gitignore b/.gitignore index 9f9f67b3..a90aa1fc 100644 --- a/.gitignore +++ b/.gitignore @@ -31,6 +31,10 @@ _opam/ # Rust working directory rust-tests/target/ +# F* +.depend +*.hints + # Misc /fstar-tests *~ -- cgit v1.2.3 From 7f06278bd0b43426e88632afcd8e5633c5ab0a1e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Jun 2022 04:40:43 +0200 Subject: Update the Makefiles --- tests/Makefile.template | 5 +---- tests/betree/Makefile | 5 +---- tests/hashmap/Makefile | 5 +---- tests/hashmap_on_disk/Makefile | 5 +---- tests/misc/Makefile | 5 +---- 5 files changed, 5 insertions(+), 20 deletions(-) diff --git a/tests/Makefile.template b/tests/Makefile.template index fed1a280..ea838d2d 100644 --- a/tests/Makefile.template +++ b/tests/Makefile.template @@ -21,10 +21,7 @@ ifeq (,$(filter %-in,$(MAKECMDGOALS))) ifndef NODEPEND ifndef MAKE_RESTARTS .depend: .FORCE - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ - --extract 'krml:*' \ - --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ - > $@ + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ .PHONY: .FORCE .FORCE: diff --git a/tests/betree/Makefile b/tests/betree/Makefile index fed1a280..ea838d2d 100644 --- a/tests/betree/Makefile +++ b/tests/betree/Makefile @@ -21,10 +21,7 @@ ifeq (,$(filter %-in,$(MAKECMDGOALS))) ifndef NODEPEND ifndef MAKE_RESTARTS .depend: .FORCE - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ - --extract 'krml:*' \ - --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ - > $@ + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ .PHONY: .FORCE .FORCE: diff --git a/tests/hashmap/Makefile b/tests/hashmap/Makefile index fed1a280..ea838d2d 100644 --- a/tests/hashmap/Makefile +++ b/tests/hashmap/Makefile @@ -21,10 +21,7 @@ ifeq (,$(filter %-in,$(MAKECMDGOALS))) ifndef NODEPEND ifndef MAKE_RESTARTS .depend: .FORCE - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ - --extract 'krml:*' \ - --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ - > $@ + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ .PHONY: .FORCE .FORCE: diff --git a/tests/hashmap_on_disk/Makefile b/tests/hashmap_on_disk/Makefile index fed1a280..ea838d2d 100644 --- a/tests/hashmap_on_disk/Makefile +++ b/tests/hashmap_on_disk/Makefile @@ -21,10 +21,7 @@ ifeq (,$(filter %-in,$(MAKECMDGOALS))) ifndef NODEPEND ifndef MAKE_RESTARTS .depend: .FORCE - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ - --extract 'krml:*' \ - --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ - > $@ + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ .PHONY: .FORCE .FORCE: diff --git a/tests/misc/Makefile b/tests/misc/Makefile index fed1a280..ea838d2d 100644 --- a/tests/misc/Makefile +++ b/tests/misc/Makefile @@ -21,10 +21,7 @@ ifeq (,$(filter %-in,$(MAKECMDGOALS))) ifndef NODEPEND ifndef MAKE_RESTARTS .depend: .FORCE - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \ - --extract 'krml:*' \ - --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ - > $@ + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ .PHONY: .FORCE .FORCE: -- cgit v1.2.3 From f24f1043e72cddad2b29b09b79649ffc5e1d7c42 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Jun 2022 06:19:11 +0200 Subject: Update eval_operand_prepare to not give a value to the continuation --- src/Cps.ml | 37 +++++++++-- src/InterpreterExpansion.ml | 31 +++++---- src/InterpreterExpressions.ml | 146 +++++++++++++++++++++++++++--------------- src/InterpreterStatements.ml | 76 ++++++++++------------ 4 files changed, 181 insertions(+), 109 deletions(-) diff --git a/src/Cps.ml b/src/Cps.ml index d7c50f26..2d7dd2be 100644 --- a/src/Cps.ml +++ b/src/Cps.ml @@ -77,7 +77,6 @@ let comp_ret_val (f : (V.typed_value -> m_fun) -> m_fun) comp f g let apply (f : cm_fun) (g : m_fun) : m_fun = fun ctx -> f g ctx - let id_cm_fun : cm_fun = fun cf ctx -> cf ctx (** If we have a list of [inputs] of type `'a list` and a function [f] which @@ -92,7 +91,37 @@ let id_cm_fun : cm_fun = fun cf ctx -> cf ctx See the unit test below for an illustration. *) -let fold_left_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd) +let fold_left_apply_continuation (f : 'a -> ('c -> 'd) -> 'c -> 'd) + (inputs : 'a list) (cf : 'c -> 'd) : 'c -> 'd = + let rec eval_list (inputs : 'a list) (cf : 'c -> 'd) : 'c -> 'd = + fun ctx -> + match inputs with + | [] -> cf ctx + | x :: inputs -> comp (f x) (fun cf -> eval_list inputs cf) cf ctx + in + eval_list inputs cf + +(** Unit test/example for [fold_left_apply_continuation] *) +let _ = + fold_left_apply_continuation + (fun x cf (ctx : int) -> cf (ctx + x)) + [ 1; 20; 300; 4000 ] + (fun (ctx : int) -> assert (ctx = 4321)) + 0 + +(** If we have a list of [inputs] of type `'a list` and a function [f] which + evaluates one element of type `'a` to compute a result of type `'b` before + giving it to a continuation, the following function performs a fold operation: + it evaluates all the inputs one by one by accumulating the results in a list, + and gives the list to a continuation. + + Note that we make sure that the results are listed in the order in + which they were computed (the first element of the list is the result + of applying [f] to the first element of the inputs). + + See the unit test below for an illustration. + *) +let fold_left_list_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd) (inputs : 'a list) (cf : 'b list -> 'c -> 'd) : 'c -> 'd = let rec eval_list (inputs : 'a list) (cf : 'b list -> 'c -> 'd) (outputs : 'b list) : 'c -> 'd = @@ -104,9 +133,9 @@ let fold_left_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd) in eval_list inputs cf [] -(** Unit test/example for [fold_left_apply_continuation] *) +(** Unit test/example for [fold_left_list_apply_continuation] *) let _ = - fold_left_apply_continuation + fold_left_list_apply_continuation (fun x cf (ctx : unit) -> cf (10 + x) ctx) [ 0; 1; 2; 3; 4 ] (fun values _ctx -> assert (values = [ 10; 11; 12; 13; 14 ])) diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 0b65a372..c34051a8 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -188,8 +188,6 @@ let replace_symbolic_values (at_most_once : bool) in (* Apply the substitution *) let ctx = obj#visit_eval_ctx None ctx in - (* Check that we substituted *) - assert !replaced; (* Return *) ctx @@ -469,8 +467,24 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config) let seel = List.map fst see_cf_l in S.synthesize_symbolic_expansion sv sv_place seel subterms -(** Expand a symbolic value which is not an enumeration with several variants - (i.e., in a situation where it doesn't lead to branching). +(** Expand a symbolic boolean *) +let expand_symbolic_bool (config : C.config) (sp : V.symbolic_value) + (sp_place : SA.mplace option) (cf_true : m_fun) (cf_false : m_fun) : m_fun = + fun ctx -> + (* Compute the expanded value *) + let original_sv = sp in + let original_sv_place = sp_place in + let rty = original_sv.V.sv_ty in + assert (rty = T.Bool); + (* Expand the symbolic value to true or false and continue execution *) + let see_true = V.SeConcrete (V.Bool true) in + let see_false = V.SeConcrete (V.Bool false) in + let seel = [ (Some see_true, cf_true); (Some see_false, cf_false) ] in + (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *) + apply_branching_symbolic_expansions_non_borrow config original_sv + original_sv_place seel ctx + +(** Expand a symbolic value. [allow_branching]: if `true` we can branch (by expanding enumerations with stricly more than one variant), otherwise we can't. @@ -554,14 +568,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) (* Booleans *) | T.Bool -> assert allow_branching; - (* Expand the symbolic value to true or false and continue execution *) - let see_true = V.SeConcrete (V.Bool true) in - let see_false = V.SeConcrete (V.Bool false) in - let seel = [ see_true; see_false ] in - let seel = List.map (fun see -> (Some see, cf)) seel in - (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *) - apply_branching_symbolic_expansions_non_borrow config original_sv - original_sv_place seel ctx + expand_symbolic_bool config sp sp_place cf cf ctx | _ -> raise (Failure ("expand_symbolic_value: unexpected type: " ^ T.show_rty rty)) diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 4549365d..bdcadf3a 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -48,13 +48,24 @@ let expand_primitively_copyable_at_place (config : C.config) (* Apply *) expand cf ctx +(** Read a place (CPS-style function *) +let read_place (config : C.config) (access : access_kind) (p : E.place) + (cf : V.typed_value -> m_fun) : m_fun = + fun ctx -> + let v = read_place_unwrap config access p ctx in + cf v ctx + (** Small utility. + Prepare the access to a place in a right-value (typically an operand) by + reorganizing the environment. + [expand_prim_copy]: if true, expand the symbolic values which are primitively copyable and contain borrows. *) -let prepare_rplace (config : C.config) (expand_prim_copy : bool) - (access : access_kind) (p : E.place) (cf : V.typed_value -> m_fun) : m_fun = +let access_rplace_reorganize_and_read (config : C.config) + (expand_prim_copy : bool) (access : access_kind) (p : E.place) + (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> let cc = update_ctx_along_read_place config access p in let cc = comp cc (end_loans_at_place config access p) in @@ -63,13 +74,16 @@ let prepare_rplace (config : C.config) (expand_prim_copy : bool) comp cc (expand_primitively_copyable_at_place config access p) else cc in - let read_place cf : m_fun = - fun ctx -> - let v = read_place_unwrap config access p ctx in - cf v ctx - in + let read_place = read_place config access p in comp cc read_place cf ctx +let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool) + (access : access_kind) (p : E.place) : cm_fun = + fun cf ctx -> + access_rplace_reorganize_and_read config expand_prim_copy access p + (fun _v -> cf) + ctx + (** Convert an operand constant operand value to a typed value *) let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) (cv : E.operand_constant_value) : V.typed_value = @@ -119,10 +133,10 @@ let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) | _, ConstantAdt _ | _, ConstantValue _ -> failwith "Improperly typed constant value" -(** Prepare the evaluation of an operand. +(** Reorganize the environment in preparation for the evaluation of an operand. - Evaluating an operand requires updating the context to get access to a - given place (by ending borrows, expanding symbolic values...) then + Evaluating an operand requires reorganizing the environment to get access + to a given place (by ending borrows, expanding symbolic values...) then applying the operand operation (move, copy, etc.). Sometimes, we want to decouple the two operations. @@ -136,7 +150,7 @@ let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) dest <- f(move x, move y); ... ``` - Because of the way end_borrow is implemented, when giving back the borrow + Because of the way `end_borrow` is implemented, when giving back the borrow `l0` upon evaluating `move y`, we won't notice that `shared_borrow l0` has disappeared from the environment (it has been moved and not assigned yet, and so is hanging in "thin air"). @@ -144,51 +158,49 @@ let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) By first "preparing" the operands evaluation, we make sure no such thing happens. To be more precise, we make sure all the updates to borrows triggered by access *and* move operations have already been applied. + + Rk.: in the formalization, we always have an explicit "reorganization" step + in the rule premises, before the actual operand evaluation. - As a side note: doing this is actually not completely necessary because when + Rk.: doing this is actually not completely necessary because when generating MIR, rustc introduces intermediate assignments for all the function parameters. Still, it is better for soundness purposes, and corresponds to - what we do in the formal semantics. + what we do in the formalization (because we don't enforce constraints + in the formalization). *) -let eval_operand_prepare (config : C.config) (op : E.operand) - (cf : V.typed_value -> m_fun) : m_fun = - fun ctx -> - let prepare (cf : V.typed_value -> m_fun) : m_fun = - fun ctx -> +let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) : + cm_fun = + fun cf ctx -> + let prepare : cm_fun = + fun cf ctx -> match op with - | Expressions.Constant (ty, cv) -> - let v = operand_constant_value_to_typed_value ctx ty cv in - cf v ctx + | Expressions.Constant _ -> + (* No need to reorganize the context *) + cf ctx | Expressions.Copy p -> (* Access the value *) let access = Read in (* Expand the symbolic values, if necessary *) let expand_prim_copy = true in - prepare_rplace config expand_prim_copy access p cf ctx + access_rplace_reorganize config expand_prim_copy access p cf ctx | Expressions.Move p -> (* Access the value *) let access = Move in let expand_prim_copy = false in - prepare_rplace config expand_prim_copy access p cf ctx + access_rplace_reorganize config expand_prim_copy access p cf ctx in - (* Sanity check *) - let check cf v : m_fun = - fun ctx -> - assert (not (bottom_in_value ctx.ended_regions v)); - cf v ctx - in - (* Compose and apply *) - comp prepare check cf ctx + (* Apply *) + prepare cf ctx -(** Evaluate an operand. *) -let eval_operand (config : C.config) (op : E.operand) +(** Evaluate an operand, without reorganizing the context before *) +let eval_operand_no_reorganize (config : C.config) (op : E.operand) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> (* Debug *) log#ldebug (lazy - ("eval_operand: op: " ^ operand_to_string ctx op ^ "\n- ctx:\n" - ^ eval_ctx_to_string ctx ^ "\n")); + ("eval_operand_no_reorganize: op: " ^ operand_to_string ctx op + ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n")); (* Evaluate *) match op with | Expressions.Constant (ty, cv) -> @@ -197,8 +209,7 @@ let eval_operand (config : C.config) (op : E.operand) | Expressions.Copy p -> (* Access the value *) let access = Read in - let expand_prim_copy = true in - let cc = prepare_rplace config expand_prim_copy access p in + let cc = read_place config access p in (* Copy the value *) let copy cf v : m_fun = fun ctx -> @@ -208,8 +219,8 @@ let eval_operand (config : C.config) (op : E.operand) Option.is_none (find_first_primitively_copyable_sv_with_borrows ctx.type_context.type_infos v)); - let allow_adt_copy = false in (* Actually perform the copy *) + let allow_adt_copy = false in let ctx, v = copy_value allow_adt_copy config ctx v in (* Continue *) cf v ctx @@ -219,11 +230,11 @@ let eval_operand (config : C.config) (op : E.operand) | Expressions.Move p -> (* Access the value *) let access = Move in - let expand_prim_copy = false in - let cc = prepare_rplace config expand_prim_copy access p in + let cc = read_place config access p in (* Move the value *) let move cf v : m_fun = fun ctx -> + (* Check that there are no bottoms in the value we are about to move *) assert (not (bottom_in_value ctx.ended_regions v)); let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in match write_place config access p bottom ctx with @@ -233,24 +244,49 @@ let eval_operand (config : C.config) (op : E.operand) (* Compose and apply *) comp cc move cf ctx +(** Evaluate an operand. + + Reorganize the context, then evaluate the operand. + + **Warning**: this function shouldn't be used to evaluate a list of + operands (for a function call, for instance): we must do *one* reorganization + of the environment, before evaluating all the operands at once. + Use [`eval_operands`] instead. + *) +let eval_operand (config : C.config) (op : E.operand) + (cf : V.typed_value -> m_fun) : m_fun = + fun ctx -> + (* Debug *) + log#ldebug + (lazy + ("eval_operand: op: " ^ operand_to_string ctx op ^ "\n- ctx:\n" + ^ eval_ctx_to_string ctx ^ "\n")); + (* We reorganize the context, then evaluate the operand *) + comp + (prepare_eval_operand_reorganize config op) + (eval_operand_no_reorganize config op) + cf ctx + (** Small utility. - See [eval_operand_prepare]. + See [prepare_eval_operand_reorganize]. *) -let eval_operands_prepare (config : C.config) (ops : E.operand list) - (cf : V.typed_value list -> m_fun) : m_fun = - fold_left_apply_continuation (eval_operand_prepare config) ops cf +let prepare_eval_operands_reorganize (config : C.config) (ops : E.operand list) + : cm_fun = + fold_left_apply_continuation (prepare_eval_operand_reorganize config) ops (** Evaluate several operands. *) let eval_operands (config : C.config) (ops : E.operand list) (cf : V.typed_value list -> m_fun) : m_fun = fun ctx -> (* Prepare the operands *) - let prepare = eval_operands_prepare config ops in + let prepare = prepare_eval_operands_reorganize config ops in (* Evaluate the operands *) - let eval = fold_left_apply_continuation (eval_operand config) ops in + let eval = + fold_left_list_apply_continuation (eval_operand_no_reorganize config) ops + in (* Compose and apply *) - comp prepare (fun cf (_ : V.typed_value list) -> eval cf) cf ctx + comp prepare eval cf ctx let eval_two_operands (config : C.config) (op1 : E.operand) (op2 : E.operand) (cf : V.typed_value * V.typed_value -> m_fun) : m_fun = @@ -469,7 +505,9 @@ let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place) (* Access the value *) let access = Read in let expand_prim_copy = false in - let prepare = prepare_rplace config expand_prim_copy access p in + let prepare = + access_rplace_reorganize_and_read config expand_prim_copy access p + in (* Read the value *) let read (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun = (* The value may be shared: we need to ignore the shared loans *) @@ -507,7 +545,9 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place) (* Access the value *) let access = Read in let expand_prim_copy = false in - let prepare = prepare_rplace config expand_prim_copy access p in + let prepare = + access_rplace_reorganize_and_read config expand_prim_copy access p + in (* Read the value *) let read (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun = fun ctx -> @@ -539,7 +579,9 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) (* Access the value *) let access = if bkind = E.Shared then Read else Write in let expand_prim_copy = false in - let prepare = prepare_rplace config expand_prim_copy access p in + let prepare = + access_rplace_reorganize_and_read config expand_prim_copy access p + in (* Evaluate the borrowing operation *) let eval (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun = fun ctx -> @@ -580,7 +622,9 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) (* Access the value *) let access = Write in let expand_prim_copy = false in - let prepare = prepare_rplace config expand_prim_copy access p in + let prepare = + access_rplace_reorganize_and_read config expand_prim_copy access p + in (* Evaluate the borrowing operation *) let eval (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun = fun ctx -> diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 1083d643..e2775a1d 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -150,13 +150,10 @@ let eval_assertion_concrete (config : C.config) (assertion : A.assertion) : *) let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun = fun cf ctx -> - (* There may be a symbolic expansion, so don't fully evaluate the operand - * (if we moved the value, we can't expand it because it is hanging in - * thin air, outside of the environment...): simply update the environment - * to make sure we have access to the value we want to check. *) - let prepare = eval_operand_prepare config assertion.cond in + (* Evaluate the operand *) + let eval_op = eval_operand config assertion.cond in (* Evaluate the assertion *) - let eval cf (v : V.typed_value) : m_fun = + let eval_assert cf (v : V.typed_value) : m_fun = fun ctx -> assert (v.ty = T.Bool); (* We make a choice here: we could completely decouple the concrete and @@ -171,20 +168,22 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun = | Symbolic sv -> assert (config.mode = C.SymbolicMode); assert (sv.V.sv_ty = T.Bool); - (* Expand the symbolic value, then call the evaluation function for the - * non-symbolic case *) - let allow_branching = true in + (* Expand the symbolic value and call the proper continuation functions + * for the true and false cases - TODO: call an "assert" function instead *) + let cf_true : m_fun = fun ctx -> cf Unit ctx in + let cf_false : m_fun = fun ctx -> cf Panic ctx in let expand = - expand_symbolic_value config allow_branching sv + expand_symbolic_bool config sv (S.mk_opt_place_from_op assertion.cond ctx) + cf_true cf_false in - comp expand (eval_assertion_concrete config assertion) cf ctx + expand ctx | _ -> raise (Failure ("Expected a boolean, got: " ^ typed_value_to_string ctx v)) in (* Compose and apply *) - comp prepare eval cf ctx + comp eval_op eval_assert cf ctx (** Updates the discriminant of a value at a given place. @@ -823,8 +822,14 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = comp cf_eval_rvalue cf_assign cf ctx | A.FakeRead p -> let expand_prim_copy = false in - let cf_prepare = prepare_rplace config expand_prim_copy Read p in - let cf_continue cf _ = cf in + let cf_prepare cf = + access_rplace_reorganize_and_read config expand_prim_copy Read p cf + in + let cf_continue cf v : m_fun = + fun ctx -> + assert (not (bottom_in_value ctx.ended_regions v)); + cf ctx + in comp cf_prepare cf_continue (cf Unit) ctx | A.SetDiscriminant (p, variant_id) -> set_discriminant config p variant_id cf ctx @@ -905,7 +910,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : * (and would thus floating in thin air...)! * *) (* Prepare the operand *) - let cf_prepare_op cf : m_fun = eval_operand_prepare config op cf in + let cf_eval_op cf : m_fun = eval_operand config op cf in (* Match on the targets *) let cf_match (cf : st_m_fun) (op_v : V.typed_value) : m_fun = fun ctx -> @@ -913,39 +918,29 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : | A.If (st1, st2) -> ( match op_v.value with | V.Concrete (V.Bool b) -> - (* Evaluate the operand *) - let cf_eval_op cf : m_fun = eval_operand config op cf in (* Evaluate the if and the branch body *) - let cf_branch cf op_v' : m_fun = - assert (op_v' = op_v); + let cf_branch cf : m_fun = (* Branch *) if b then eval_statement config st1 cf else eval_statement config st2 cf in (* Compose the continuations *) - comp cf_eval_op cf_branch cf ctx + cf_branch cf ctx | V.Symbolic sv -> - (* Expand the symbolic value *) - let allows_branching = true in - let cf_expand cf = - expand_symbolic_value config allows_branching sv - (S.mk_opt_place_from_op op ctx) - cf - in - (* Retry *) - let cf_eval_if cf = eval_switch config op tgts cf in - (* Compose *) - comp cf_expand cf_eval_if cf ctx + (* Expand the symbolic boolean, and continue by evaluating + * the branches *) + let cf_true : m_fun = eval_statement config st1 cf in + let cf_false : m_fun = eval_statement config st2 cf in + expand_symbolic_bool config sv + (S.mk_opt_place_from_op op ctx) + cf_true cf_false ctx | _ -> raise (Failure "Inconsistent state")) | A.SwitchInt (int_ty, stgts, otherwise) -> ( match op_v.value with | V.Concrete (V.Scalar sv) -> - (* Evaluate the operand *) - let cf_eval_op cf = eval_operand config op cf in (* Evaluate the branch *) - let cf_eval_branch cf op_v' = + let cf_eval_branch cf = (* Sanity check *) - assert (op_v' = op_v); assert (sv.V.int_ty = int_ty); (* Find the branch *) match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with @@ -953,13 +948,10 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : | Some (_, tgt) -> eval_statement config tgt cf in (* Compose *) - comp cf_eval_op cf_eval_branch cf ctx + cf_eval_branch cf ctx | V.Symbolic sv -> - (* Expand the symbolic value - note that contrary to the boolean - * case, we can't expand then retry, because when switching over - * arbitrary integers we need to have an `otherwise` case, in - * which the scrutinee remains symbolic: if we expand the symbolic, - * reevaluate the switch, we loop... *) + (* Expand the symbolic value and continue by evaluating the + * proper branches *) let stgts = List.map (fun (cv, tgt_st) -> (cv, eval_statement config tgt_st cf)) @@ -984,7 +976,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : | _ -> raise (Failure "Inconsistent state")) in (* Compose the continuations *) - comp cf_prepare_op cf_match cf ctx + comp cf_eval_op cf_match cf ctx (** Evaluate a function call (auxiliary helper for [eval_statement]) *) and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = -- cgit v1.2.3 From 8c3dc80d255ba2000d35c0bcdf9dbe927215bb81 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Jun 2022 06:51:08 +0200 Subject: Add `can_end` in `abs` and use it for the return abs when generating the backward functions --- src/Interpreter.ml | 43 +++++++++++++++++++++++++++++-------------- src/InterpreterBorrows.ml | 3 +++ src/InterpreterStatements.ml | 16 ++++++++++++++-- src/LlbcAstUtils.ml | 3 ++- src/Values.ml | 27 +++++++++++---------------- 5 files changed, 59 insertions(+), 33 deletions(-) diff --git a/src/Interpreter.ml b/src/Interpreter.ml index f6ae268d..cbbf2b2e 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -86,9 +86,10 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context) in (ctx, avalues) in + let region_can_end _ = true in let ctx = create_push_abstractions_from_abs_region_groups call_id V.SynthInput - inst_sg.A.regions_hierarchy compute_abs_avalues ctx + inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx in (* Split the variables between return var, inputs and remaining locals *) let body = Option.get fdef.body in @@ -127,6 +128,21 @@ let evaluate_function_symbolic_synthesize_backward_from_return (* Move the return value out of the return variable *) let cf_pop_frame = ctx_pop_frame config in + (* We need to find the parents regions/abstractions of the region we + * will end - this will allow us to, first, mark the other return + * regions as non-endable, and, second, end those parent regions in + * proper order. *) + let parent_rgs = list_parent_region_groups sg back_id in + let parent_input_abs_ids = + T.RegionGroupId.mapi + (fun rg_id rg -> + if T.RegionGroupId.Set.mem rg_id parent_rgs then Some rg.T.id else None) + inst_sg.regions_hierarchy + in + let parent_input_abs_ids = + List.filter_map (fun x -> x) parent_input_abs_ids + in + (* Insert the return value in the return abstractions (by applying * borrow projections) *) let cf_consume_ret ret_value ctx = @@ -139,10 +155,20 @@ let evaluate_function_symbolic_synthesize_backward_from_return in (ctx, [ avalue ]) in - (* Initialize and insert the abstractions in the context *) + + (* Initialize and insert the abstractions in the context. + * + * We take care of disallowing ending the return regions which we + * shouldn't end (see the documentation of the `can_end` field of [abs] + * for more information. *) + let parent_and_current_rgs = T.RegionGroupId.Set.add back_id parent_rgs in + let region_can_end rid = + T.RegionGroupId.Set.mem rid parent_and_current_rgs + in + assert (region_can_end back_id); let ctx = create_push_abstractions_from_abs_region_groups ret_call_id V.SynthRet - ret_inst_sg.A.regions_hierarchy compute_abs_avalues ctx + ret_inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx in (* We now need to end the proper *input* abstractions - pay attention @@ -150,17 +176,6 @@ let evaluate_function_symbolic_synthesize_backward_from_return * abstractions (of course, the corresponding return abstractions will * automatically be ended, because they consumed values coming from the * input abstractions...) *) - let parent_rgs = list_parent_region_groups sg back_id in - let parent_input_abs_ids = - T.RegionGroupId.mapi - (fun rg_id rg -> - if T.RegionGroupId.Set.mem rg_id parent_rgs then Some rg.T.id - else None) - inst_sg.regions_hierarchy - in - let parent_input_abs_ids = - List.filter_map (fun x -> x) parent_input_abs_ids - in (* End the parent abstractions and the current abstraction - note that we * end them in an order which follows the regions hierarchy: it should lead * to generated code which has a better consistency between the parent diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index f5f3a8fa..26374bf7 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -985,6 +985,9 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids) (* Lookup the abstraction *) let abs = C.ctx_lookup_abs ctx abs_id in + (* Check that we can end the abstraction *) + assert abs.can_end; + (* End the parent abstractions first *) let cc = end_abstractions config chain abs.parents in let cc = diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index e2775a1d..585fa828 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -677,9 +677,13 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) : Create abstractions (with no avalues, which have to be inserted afterwards) from a list of abs region groups. + + [region_can_end]: gives the region groups from which we generate functions + which can end or not. *) let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id) - (kind : V.abs_kind) (rgl : A.abs_region_group list) : V.abs list = + (kind : V.abs_kind) (rgl : A.abs_region_group list) + (region_can_end : T.RegionGroupId.id -> bool) : V.abs list = (* We use a reference to progressively create a map from abstraction ids * to set of ancestor regions. Note that abs_to_ancestors_regions[abs_id] * returns the union of: @@ -714,6 +718,7 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id) let ancestors_regions_union_current_regions = T.RegionId.Set.union ancestors_regions regions in + let can_end = region_can_end back_id in abs_to_ancestors_regions := V.AbstractionId.Map.add abs_id ancestors_regions_union_current_regions !abs_to_ancestors_regions; @@ -723,6 +728,7 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id) call_id; back_id; kind; + can_end; parents; original_parents; regions; @@ -737,6 +743,9 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id) Create a list of abstractions from a list of regions groups, and insert them in the context. + + [region_can_end]: gives the region groups from which we generate functions + which can end or not. [compute_abs_avalues]: this function must compute, given an initialized, empty (i.e., with no avalues) abstraction, compute the avalues which @@ -746,12 +755,14 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id) *) let create_push_abstractions_from_abs_region_groups (call_id : V.FunCallId.id) (kind : V.abs_kind) (rgl : A.abs_region_group list) + (region_can_end : T.RegionGroupId.id -> bool) (compute_abs_avalues : V.abs -> C.eval_ctx -> C.eval_ctx * V.typed_avalue list) (ctx : C.eval_ctx) : C.eval_ctx = (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) let empty_absl = create_empty_abstractions_from_abs_region_groups call_id kind rgl + region_can_end in (* Compute and add the avalues to the abstractions, the insert the abstractions @@ -1152,9 +1163,10 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) in (* Actually initialize and insert the abstractions *) let call_id = C.fresh_fun_call_id () in + let region_can_end _ = true in let ctx = create_push_abstractions_from_abs_region_groups call_id V.FunCall - inst_sg.A.regions_hierarchy compute_abs_avalues ctx + inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx in (* Apply the continuation *) diff --git a/src/LlbcAstUtils.ml b/src/LlbcAstUtils.ml index 84e8e00f..0e679fca 100644 --- a/src/LlbcAstUtils.ml +++ b/src/LlbcAstUtils.ml @@ -7,7 +7,6 @@ let statement_has_loops (st : statement) : bool = let obj = object inherit [_] iter_statement - method! visit_Loop _ _ = raise Found end in @@ -38,6 +37,8 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : We don't do that in an efficient manner, but it doesn't matter. TODO: rename to "list_ancestors_..." + + This list *doesn't* include the current region. *) let rec list_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) : T.RegionGroupId.Set.t = diff --git a/src/Values.ml b/src/Values.ml index 4e45db03..4585b443 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -6,13 +6,9 @@ open Types * inside abstractions) *) module VarId = IdGen () - module BorrowId = IdGen () - module SymbolicValueId = IdGen () - module AbstractionId = IdGen () - module FunCallId = IdGen () (** A variable *) @@ -83,13 +79,9 @@ type symbolic_value = { class ['self] iter_typed_value_base = object (_self : 'self) inherit [_] VisitorsRuntime.iter - method visit_constant_value : 'env -> constant_value -> unit = fun _ _ -> () - method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> () - method visit_symbolic_value : 'env -> symbolic_value -> unit = fun _ _ -> () - method visit_ety : 'env -> ety -> unit = fun _ _ -> () end @@ -228,7 +220,6 @@ and typed_value = { value : value; ty : ety } class ['self] iter_typed_value = object (_self : 'self) inherit [_] iter_typed_value_visit_mvalue - method! visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> () end @@ -236,7 +227,6 @@ class ['self] iter_typed_value = class ['self] map_typed_value = object (_self : 'self) inherit [_] map_typed_value_visit_mvalue - method! visit_mvalue : 'env -> mvalue -> mvalue = fun _ x -> x end @@ -275,7 +265,6 @@ type abstract_shared_borrows = abstract_shared_borrow list [@@deriving show] class ['self] iter_aproj_base = object (_self : 'self) inherit [_] iter_typed_value - method visit_rty : 'env -> rty -> unit = fun _ _ -> () method visit_msymbolic_value : 'env -> msymbolic_value -> unit = @@ -286,7 +275,6 @@ class ['self] iter_aproj_base = class ['self] map_aproj_base = object (_self : 'self) inherit [_] map_typed_value - method visit_rty : 'env -> rty -> rty = fun _ ty -> ty method visit_msymbolic_value : 'env -> msymbolic_value -> msymbolic_value = @@ -374,9 +362,7 @@ type region = RegionVarId.id Types.region [@@deriving show] class ['self] iter_typed_avalue_base = object (_self : 'self) inherit [_] iter_aproj - method visit_id : 'env -> BorrowId.id -> unit = fun _ _ -> () - method visit_region : 'env -> region -> unit = fun _ _ -> () method visit_abstract_shared_borrows @@ -388,9 +374,7 @@ class ['self] iter_typed_avalue_base = class ['self] map_typed_avalue_base = object (_self : 'self) inherit [_] map_aproj - method visit_id : 'env -> BorrowId.id -> BorrowId.id = fun _ id -> id - method visit_region : 'env -> region -> region = fun _ r -> r method visit_abstract_shared_borrows @@ -798,6 +782,17 @@ type abs = { the symbolic AST, generated by the symbolic execution. *) kind : (abs_kind[@opaque]); + can_end : (bool[@opaque]); + (** Controls whether the region can be ended or not. + + This allows to "pin" some regions, and is useful when generating + backward functions. + + For instance, if we have: `fn f<'a, 'b>(...) -> (&'a mut T, &'b mut T)`, + when generating the backward function for 'a, we have to make sure we + don't need to end the return region for 'b (if it is the case, it means + the function doesn't borrow check). + *) parents : (AbstractionId.Set.t[@opaque]); (** The parent abstractions *) original_parents : (AbstractionId.id list[@opaque]); (** The original list of parents, ordered. This is used for synthesis. *) -- cgit v1.2.3 From 775b2473976075aa6458a51682f3beeee75dc17a Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 29 Jun 2022 08:50:17 +0200 Subject: Make minor modifications --- src/InterpreterBorrows.ml | 19 ++++++++++++++++--- src/InterpreterExpressions.ml | 25 ++++++++++++++++++++++++- src/InterpreterPaths.ml | 6 +++++- src/Print.ml | 2 +- 4 files changed, 46 insertions(+), 6 deletions(-) diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 26374bf7..a13ac786 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -1442,12 +1442,22 @@ let end_outer_borrows config : V.BorrowId.Set.t -> cm_fun = - it mustn't contain [Bottom] - it mustn't contain inactivated borrows TODO: this kind of checks should be put in an auxiliary helper, because - they are redundant + they are redundant. + + The loan to update mustn't be a borrowed value. *) let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> - (* Lookup the shared loan *) + (* Debug *) + log#ldebug + (lazy + ("promote_shared_loan_to_mut_loan:\n- loan: " ^ V.BorrowId.to_string l + ^ "\n- context:\n" ^ eval_ctx_to_string ctx ^ "\n")); + (* Lookup the shared loan - note that we can't promote a shared loan + * in a shared value, but we can do it in a mutably borrowed value. + * This is important because we can do: `let y = &two-phase ( *x );` + *) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } in @@ -1548,7 +1558,10 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id) the borrow we want to promote *) let bids = V.BorrowId.Set.remove l bids in let cc = end_outer_borrows config bids in - (* Promote the loan *) + (* Promote the loan - TODO: this will fail if the value contains + * any loans. In practice, it shouldn't, but we could also + * look for loans inside the value and end them before promoting + * the borrow. *) let cc = comp cc (promote_shared_loan_to_mut_loan l) in (* Promote the borrow - the value should have been checked by [promote_shared_loan_to_mut_loan] diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index bdcadf3a..6bb2baf0 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -48,11 +48,20 @@ let expand_primitively_copyable_at_place (config : C.config) (* Apply *) expand cf ctx -(** Read a place (CPS-style function *) +(** Read a place (CPS-style function). + + We also check that the value *doesn't contain bottoms or inactivated + borrows. + *) let read_place (config : C.config) (access : access_kind) (p : E.place) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> let v = read_place_unwrap config access p ctx in + (* Check that there are no bottoms in the value *) + assert (not (bottom_in_value ctx.ended_regions v)); + (* Check that there are no inactivated borrows in the value *) + assert (not (inactivated_in_value v)); + (* Call the continuation *) cf v ctx (** Small utility. @@ -60,6 +69,14 @@ let read_place (config : C.config) (access : access_kind) (p : E.place) Prepare the access to a place in a right-value (typically an operand) by reorganizing the environment. + We reorganize the environment so that: + - we can access the place (we prepare *along* the path) + - the value at the place itself doesn't contain loans (the `access_kind` + controls whether we only end mutable loans, or also shared loans). + + We also check, after the reorganization, that the value at the place + *doesn't contain any bottom nor inactivated borrows*. + [expand_prim_copy]: if true, expand the symbolic values which are primitively copyable and contain borrows. *) @@ -67,14 +84,20 @@ let access_rplace_reorganize_and_read (config : C.config) (expand_prim_copy : bool) (access : access_kind) (p : E.place) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> + (* Make sure we can evaluate the path *) let cc = update_ctx_along_read_place config access p in + (* End the proper loans at the place itself *) let cc = comp cc (end_loans_at_place config access p) in + (* Expand the copyable values which contain borrows (which are necessarily shared + * borrows) *) let cc = if expand_prim_copy then comp cc (expand_primitively_copyable_at_place config access p) else cc in + (* Read the place - note that this checks that the value doesn't contain bottoms *) let read_place = read_place config access p in + (* Compose *) comp cc read_place cf ctx let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool) diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index 52742703..edd27138 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -304,7 +304,11 @@ let access_kind_to_projection_access (access : access_kind) : projection_access lookup_shared_borrows = false; } -(** Read the value at a given place *) +(** Read the value at a given place. + + Note that we only access the value at the place, and do not check that + the value is "well-formed" (for instance that it doesn't contain bottoms). + *) let read_place (config : C.config) (access : access_kind) (p : E.place) (ctx : C.eval_ctx) : V.typed_value path_access_result = let access = access_kind_to_projection_access access in diff --git a/src/Print.ml b/src/Print.ml index 8e29bc67..af6fc982 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -948,7 +948,7 @@ module LlbcAst = struct match st with | A.Assign (p, rv) -> indent ^ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv - | A.FakeRead p -> "fake_read " ^ place_to_string fmt p + | A.FakeRead p -> indent ^ "fake_read " ^ place_to_string fmt p | A.SetDiscriminant (p, variant_id) -> (* TODO: improve this to lookup the variant name by using the def id *) indent ^ "set_discriminant(" ^ place_to_string fmt p ^ ", " -- cgit v1.2.3 From 4f33892c81cdaf6aefaad9b7cef1456dcfead67c Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 30 Jun 2022 06:46:52 +0200 Subject: Take failing rvalues into account in FunsAnalysis.analyze_fun_decls --- src/ExpressionsUtils.ml | 10 ++++++++++ src/FunsAnalysis.ml | 8 ++++++++ src/PureUtils.ml | 18 ------------------ src/SymbolicToPure.ml | 5 ++++- 4 files changed, 22 insertions(+), 19 deletions(-) create mode 100644 src/ExpressionsUtils.ml diff --git a/src/ExpressionsUtils.ml b/src/ExpressionsUtils.ml new file mode 100644 index 00000000..c3ccfb15 --- /dev/null +++ b/src/ExpressionsUtils.ml @@ -0,0 +1,10 @@ +module E = Expressions + +let unop_can_fail (unop : E.unop) : bool = + match unop with Neg | Cast _ -> true | Not -> false + +let binop_can_fail (binop : E.binop) : bool = + match binop with + | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt -> false + | Div | Rem | Add | Sub | Mul -> true + | Shl | Shr -> raise Errors.Unimplemented diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml index dc205eb9..b8dd17d8 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -9,6 +9,7 @@ open LlbcAst open Modules +module EU = ExpressionsUtils type fun_info = { can_fail : bool; @@ -57,6 +58,13 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) can_fail := true; super#visit_Assert env a + method! visit_rvalue _env rv = + match rv with + | Use _ | Ref _ | Discriminant _ | Aggregate _ -> () + | UnaryOp (uop, _) -> can_fail := EU.unop_can_fail uop || !can_fail + | BinaryOp (bop, _, _) -> + can_fail := EU.binop_can_fail bop || !can_fail + method! visit_Call env call = (match call.func with | Regular id -> diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 992b8cb8..8d3b5258 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -11,11 +11,8 @@ module RegularFunIdOrderedType = struct type t = regular_fun_id let compare = compare_regular_fun_id - let to_string = show_regular_fun_id - let pp_t = pp_regular_fun_id - let show_t = show_regular_fun_id end @@ -25,26 +22,14 @@ module FunIdOrderedType = struct type t = fun_id let compare = compare_fun_id - let to_string = show_fun_id - let pp_t = pp_fun_id - let show_t = show_fun_id end module FunIdMap = Collections.MakeMap (FunIdOrderedType) module FunIdSet = Collections.MakeSet (FunIdOrderedType) -(* TODO : move *) -let binop_can_fail (binop : E.binop) : bool = - match binop with - | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt -> false - | Div | Rem | Add | Sub | Mul -> true - | Shl | Shr -> raise Errors.Unimplemented - -(*let mk_arrow_ty (arg_ty : ty) (ret_ty : ty) : ty = Arrow (arg_ty, ret_ty)*) - let dest_arrow_ty (ty : ty) : ty * ty = match ty with | Arrow (arg_ty, ret_ty) -> (arg_ty, ret_ty) @@ -72,7 +57,6 @@ let ty_substitute (tsubst : TypeVarId.id -> ty) (ty : ty) : ty = let obj = object inherit [_] map_ty - method! visit_TypeVar _ var_id = tsubst var_id end in @@ -198,7 +182,6 @@ let remove_meta (e : texpression) : texpression = let obj = object inherit [_] map_expression as super - method! visit_Meta env _ e = super#visit_expression env e.e end in @@ -414,7 +397,6 @@ let type_decl_is_enum (def : T.type_decl) : bool = match def.kind with T.Struct _ -> false | Enum _ -> true | Opaque -> false let mk_state_ty : ty = Adt (Assumed State, []) - let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ]) let mk_result_fail_texpression (ty : ty) : texpression = diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 42479a6e..4c2ba4c8 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -478,6 +478,9 @@ let get_fun_effect_info (fun_infos : FA.fun_info FunDeclId.Map.t) let info = FunDeclId.Map.find fid fun_infos in let input_state = info.stateful in let output_state = input_state && gid = None in + (* We ignore on purpose info.can_fail: the result of the analysis is not + * used yet to adjust the translation so that the functions which syntactically + * can't fail don't use an error monad. *) { can_fail = true; input_state; output_state } | A.Assumed aid -> { @@ -1191,7 +1194,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression) assert (int_ty0 = int_ty1); let effect_info = { - can_fail = binop_can_fail binop; + can_fail = ExpressionsUtils.binop_can_fail binop; input_state = false; output_state = false; } -- cgit v1.2.3