summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore4
-rw-r--r--Makefile15
-rw-r--r--README.md21
-rw-r--r--src/Cps.ml37
-rw-r--r--src/ExpressionsUtils.ml10
-rw-r--r--src/FunsAnalysis.ml22
-rw-r--r--src/Interpreter.ml43
-rw-r--r--src/InterpreterBorrows.ml22
-rw-r--r--src/InterpreterExpansion.ml31
-rw-r--r--src/InterpreterExpressions.ml191
-rw-r--r--src/InterpreterPaths.ml6
-rw-r--r--src/InterpreterStatements.ml92
-rw-r--r--src/LlbcAstUtils.ml3
-rw-r--r--src/Print.ml2
-rw-r--r--src/PureUtils.ml18
-rw-r--r--src/SymbolicToPure.ml2
-rw-r--r--src/Values.ml27
-rw-r--r--tests/Makefile19
-rw-r--r--tests/Makefile.template48
-rw-r--r--tests/betree/Makefile48
-rw-r--r--tests/hashmap/Hashmap.Funs.fst23
-rw-r--r--tests/hashmap/Hashmap.Properties.fst189
-rw-r--r--tests/hashmap/Makefile48
-rw-r--r--tests/hashmap/Primitives.fst3
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Funs.fst25
-rw-r--r--tests/hashmap_on_disk/Makefile48
-rw-r--r--tests/hashmap_on_disk/Primitives.fst3
-rw-r--r--tests/misc/Constants.fst132
-rw-r--r--tests/misc/Makefile50
-rw-r--r--tests/misc/NoNestedBorrows.fst28
30 files changed, 790 insertions, 420 deletions
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
*~
diff --git a/Makefile b/Makefile
index 0fc3fcf4..aba2a67b 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-all: build-test
+all: build-test-verify
CHARON_HOME = ../charon
CHARON_EXEC = $(CHARON_HOME)/charon
@@ -18,22 +18,27 @@ OPTIONS ?=
TRANS_OPTIONS := -test-trans-units $(OPTIONS)
SUBDIR :=
-# Build the project and test it
-.PHONY: build-test
-build-test: build test
+# Build the project, test it and verify the generated files
+.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-constants \
trans-nll-betree_nll trans-nll-betree_main \
+# Verify the F* files generated by the translation
+.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/README.md b/README.md
index f31ae3b0..c7b98b5e 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,14 +73,11 @@ 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.
- Note that interior mutability is mostly anecdotal in sequential execution,
- but necessary for concurrent execution (it is exploited by the synchronisation
- primitives).
+ true aliasing: we will probably have to use a low-level memory model to address
+ this issue.
+ 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.
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/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 ca20352f..ee4f71c1 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;
@@ -50,12 +51,14 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
let divergent = ref false in
let visit_fun (f : fun_decl) : unit =
- print_endline ("@ fun: " ^ Print.fun_name_to_string f.name);
let obj =
object (self)
inherit [_] iter_statement as super
method may_fail b =
+ (* The fail flag is disabled for globals : the global body is
+ * normalised into its declaration, which is always successful.
+ *)
if f.is_global then () else
can_fail := !can_fail || b
@@ -63,8 +66,14 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
self#may_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 =
- print_string "@ dep: ";
pp_fun_id Format.std_formatter call.func;
print_newline ();
@@ -90,15 +99,18 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
super#visit_Loop env loop
end
in
- match f.body with
+ (match f.body with
| None ->
(* Opaque function *)
obj#may_fail true;
stateful := use_state
- | Some body -> obj#visit_statement () body.body
+ | Some body -> obj#visit_statement () body.body);
+ (* We ignore on purpose functions that cannot 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 := not f.is_global
in
List.iter visit_fun d;
- print_endline ("@ can_fail: " ^ Bool.to_string !can_fail);
{ can_fail = !can_fail; stateful = !stateful; divergent = !divergent }
in
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 5affea4c..f4f01ff8 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..a13ac786 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 =
@@ -1439,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
@@ -1545,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/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 57ee0526..04ad1b3c 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -7,6 +7,7 @@ open Errors
module C = Contexts
module Subst = Substitute
module L = Logging
+module PV = Print.Values
open TypesUtils
open ValuesUtils
module Inv = Invariants
@@ -49,50 +50,93 @@ let expand_primitively_copyable_at_place (config : C.config)
(* Apply *)
expand cf ctx
+(** 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.
+ 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.
*)
-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 ->
+ (* 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
- let read_place cf : m_fun =
- fun ctx ->
- let v = read_place_unwrap config access p ctx in
- cf v ctx
- 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
-(** Convert a constant operand value to a typed value *)
-let typecheck_constant_value (ty : T.ety) (cv : V.constant_value) : V.typed_value =
- (* Check the type while converting -
- * we actually need some information contained in the type *)
+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 typecheck_constant_value (ty : T.ety)
+ (cv : V.constant_value) : V.typed_value =
+ (* Check the type while converting - we actually need some information
+ * contained in the type *)
+ log#ldebug
+ (lazy
+ ("typecheck_constant_value:" ^ "\n- cv: "
+ ^ PV.constant_value_to_string cv));
match (ty, cv) with
(* Scalar, boolean... *)
- | T.Bool, (Bool v) -> { V.value = V.Concrete (Bool v); ty }
- | T.Char, (Char v) -> { V.value = V.Concrete (Char v); ty }
- | T.Str, (String v) -> { V.value = V.Concrete (String v); ty }
- | T.Integer int_ty, (V.Scalar v) ->
+ | T.Bool, Bool v -> { V.value = V.Concrete (Bool v); ty }
+ | T.Char, Char v -> { V.value = V.Concrete (Char v); ty }
+ | T.Str, String v -> { V.value = V.Concrete (String v); ty }
+ | T.Integer int_ty, V.Scalar v ->
(* Check the type and the ranges *)
assert (int_ty = v.int_ty);
assert (check_scalar_value_in_range v);
{ V.value = V.Concrete (V.Scalar v); ty }
(* Remaining cases (invalid) - listing as much as we can on purpose
(allows to catch errors at compilation if the definitions change) *)
- | _, _ -> failwith "Improperly typed constant value"
+ | _, _ ->
+ 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.
@@ -106,7 +150,7 @@ let typecheck_constant_value (ty : T.ety) (cv : V.constant_value) : V.typed_valu
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").
@@ -114,58 +158,56 @@ let typecheck_constant_value (ty : T.ety) (cv : V.constant_value) : V.typed_valu
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) ->
- cf (typecheck_constant_value ty cv) ctx
+ typecheck_constant_value ty cv |> ignore;
+ 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) -> cf (typecheck_constant_value ty cv) ctx
| 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 ->
@@ -175,8 +217,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
@@ -186,11 +228,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
@@ -200,24 +242,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 =
@@ -436,7 +503,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 *)
@@ -474,7 +543,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 ->
@@ -506,7 +577,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 ->
@@ -547,7 +620,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/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/InterpreterStatements.ml b/src/InterpreterStatements.ml
index e5564d59..8f981174 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.
@@ -678,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:
@@ -715,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;
@@ -724,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;
@@ -738,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
@@ -747,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
@@ -832,8 +842,14 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
eval_function_call config call 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
@@ -914,7 +930,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 ->
@@ -922,39 +938,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
@@ -962,13 +968,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))
@@ -993,7 +996,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 =
@@ -1169,9 +1172,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/Print.ml b/src/Print.ml
index 722f76ce..337116ec 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -940,7 +940,7 @@ module LlbcAst = struct
indent ^ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv
| A.AssignGlobal { dst; global } ->
indent ^ fmt.var_id_to_string dst ^ " := global " ^ fmt.global_decl_id_to_string global
- | 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 ^ ", "
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 84536005..a057b015 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1198,7 +1198,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;
}
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. *)
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..ea838d2d
--- /dev/null
+++ b/tests/Makefile.template
@@ -0,0 +1,48 @@
+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)) > $@
+
+.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..ea838d2d
--- /dev/null
+++ b/tests/betree/Makefile
@@ -0,0 +1,48 @@
+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)) > $@
+
+.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/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index 83c245fb..921ed142 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -188,6 +188,10 @@ let hash_map_insert_no_resize_fwd_back
end
end
+(** [core::num::u32::{8}::MAX] *)
+let core_num_u32_max_body : result u32 = Return 4294967295
+let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
+
(** [hashmap::HashMap::{0}::move_elements_from_list] *)
let rec hash_map_move_elements_from_list_fwd_back
(t : Type0) (ntable : hash_map_t t) (ls : list_t t) :
@@ -244,23 +248,24 @@ let rec hash_map_move_elements_fwd_back
(** [hashmap::HashMap::{0}::try_resize] *)
let hash_map_try_resize_fwd_back
(t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
- begin match scalar_cast U32 Usize 4294967295 with
+ let i = core_num_u32_max_c in
+ begin match scalar_cast U32 Usize i with
| Fail -> Fail
| Return max_usize ->
let capacity = vec_len (list_t t) self.hash_map_slots in
begin match usize_div max_usize 2 with
| Fail -> Fail
| Return n1 ->
- let (i, i0) = self.hash_map_max_load_factor in
- begin match usize_div n1 i with
+ let (i0, i1) = self.hash_map_max_load_factor in
+ begin match usize_div n1 i0 with
| Fail -> Fail
- | Return i1 ->
- if capacity <= i1
+ | Return i2 ->
+ if capacity <= i2
then
begin match usize_mul capacity 2 with
| Fail -> Fail
- | Return i2 ->
- begin match hash_map_new_with_capacity_fwd t i2 i i0 with
+ | Return i3 ->
+ begin match hash_map_new_with_capacity_fwd t i3 i0 i1 with
| Fail -> Fail
| Return ntable ->
begin match
@@ -268,13 +273,13 @@ let hash_map_try_resize_fwd_back
with
| Fail -> Fail
| Return (ntable0, _) ->
- Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
+ Return (Mkhash_map_t self.hash_map_num_entries (i0, i1)
ntable0.hash_map_max_load ntable0.hash_map_slots)
end
end
end
else
- Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
+ Return (Mkhash_map_t self.hash_map_num_entries (i0, i1)
self.hash_map_max_load self.hash_map_slots)
end
end
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:
/// ===========
///
diff --git a/tests/hashmap/Makefile b/tests/hashmap/Makefile
new file mode 100644
index 00000000..ea838d2d
--- /dev/null
+++ b/tests/hashmap/Makefile
@@ -0,0 +1,48 @@
+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)) > $@
+
+.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/Primitives.fst b/tests/hashmap/Primitives.fst
index fe351f3a..b3da25c2 100644
--- a/tests/hashmap/Primitives.fst
+++ b/tests/hashmap/Primitives.fst
@@ -34,6 +34,9 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
// Monadic assert(...)
let massert (b:bool) : result unit = if b then Return () else Fail
+// Unwrap a successful result by normalisation (used for globals).
+let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
+
(*** Misc *)
type char = FStar.Char.char
type string = string
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
index d01046ec..1d8ee3da 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -198,6 +198,10 @@ let hashmap_hash_map_insert_no_resize_fwd_back
end
end
+(** [core::num::u32::{8}::MAX] *)
+let core_num_u32_max_body : result u32 = Return 4294967295
+let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
+
(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
let rec hashmap_hash_map_move_elements_from_list_fwd_back
(t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) :
@@ -257,23 +261,24 @@ let rec hashmap_hash_map_move_elements_fwd_back
(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
let hashmap_hash_map_try_resize_fwd_back
(t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
- begin match scalar_cast U32 Usize 4294967295 with
+ let i = core_num_u32_max_c in
+ begin match scalar_cast U32 Usize i with
| Fail -> Fail
| Return max_usize ->
let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
begin match usize_div max_usize 2 with
| Fail -> Fail
| Return n1 ->
- let (i, i0) = self.hashmap_hash_map_max_load_factor in
- begin match usize_div n1 i with
+ let (i0, i1) = self.hashmap_hash_map_max_load_factor in
+ begin match usize_div n1 i0 with
| Fail -> Fail
- | Return i1 ->
- if capacity <= i1
+ | Return i2 ->
+ if capacity <= i2
then
begin match usize_mul capacity 2 with
| Fail -> Fail
- | Return i2 ->
- begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with
+ | Return i3 ->
+ begin match hashmap_hash_map_new_with_capacity_fwd t i3 i0 i1 with
| Fail -> Fail
| Return ntable ->
begin match
@@ -282,14 +287,14 @@ let hashmap_hash_map_try_resize_fwd_back
| Fail -> Fail
| Return (ntable0, _) ->
Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
- (i, i0) ntable0.hashmap_hash_map_max_load
+ (i0, i1) ntable0.hashmap_hash_map_max_load
ntable0.hashmap_hash_map_slots)
end
end
end
else
- Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i,
- i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
+ Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i0,
+ i1) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
end
end
end
diff --git a/tests/hashmap_on_disk/Makefile b/tests/hashmap_on_disk/Makefile
new file mode 100644
index 00000000..ea838d2d
--- /dev/null
+++ b/tests/hashmap_on_disk/Makefile
@@ -0,0 +1,48 @@
+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)) > $@
+
+.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/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst
index fe351f3a..b3da25c2 100644
--- a/tests/hashmap_on_disk/Primitives.fst
+++ b/tests/hashmap_on_disk/Primitives.fst
@@ -34,6 +34,9 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
// Monadic assert(...)
let massert (b:bool) : result unit = if b then Return () else Fail
+// Unwrap a successful result by normalisation (used for globals).
+let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
+
(*** Misc *)
type char = FStar.Char.char
type string = string
diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst
index 8419ba43..06425e64 100644
--- a/tests/misc/Constants.fst
+++ b/tests/misc/Constants.fst
@@ -5,7 +5,137 @@ open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+(** [constants::X0] *)
+let x0_body : result u32 = Return 0
+let x0_c : u32 = eval_global x0_body
+
+(** [core::num::u32::{8}::MAX] *)
+let core_num_u32_max_body : result u32 = Return 4294967295
+let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
+
+(** [constants::X1] *)
+let x1_body : result u32 = let i = core_num_u32_max_c in Return i
+let x1_c : u32 = eval_global x1_body
+
+(** [constants::X2] *)
+let x2_body : result u32 = Return 3
+let x2_c : u32 = eval_global x2_body
+
(** [constants::incr] *)
-let incr_fwd (n : u32) : u32 =
+let incr_fwd (n : u32) : result u32 =
begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end
+(** [constants::X3] *)
+let x3_body : result u32 =
+ begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end
+let x3_c : u32 = eval_global x3_body
+
+(** [constants::mk_pair0] *)
+let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = Return (x, y)
+
+(** [constants::Pair] *)
+type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; }
+
+(** [constants::mk_pair1] *)
+let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) =
+ Return (Mkpair_t x y)
+
+(** [constants::P0] *)
+let p0_body : result (u32 & u32) =
+ begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+let p0_c : (u32 & u32) = eval_global p0_body
+
+(** [constants::P1] *)
+let p1_body : result (pair_t u32 u32) =
+ begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+let p1_c : pair_t u32 u32 = eval_global p1_body
+
+(** [constants::P2] *)
+let p2_body : result (u32 & u32) = Return (0, 1)
+let p2_c : (u32 & u32) = eval_global p2_body
+
+(** [constants::P3] *)
+let p3_body : result (pair_t u32 u32) = Return (Mkpair_t 0 1)
+let p3_c : pair_t u32 u32 = eval_global p3_body
+
+(** [constants::Wrap] *)
+type wrap_t (t : Type0) = { wrap_val : t; }
+
+(** [constants::Wrap::{0}::new] *)
+let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
+ Return (Mkwrap_t val0)
+
+(** [constants::Y] *)
+let y_body : result (wrap_t i32) =
+ begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end
+let y_c : wrap_t i32 = eval_global y_body
+
+(** [constants::unwrap_y] *)
+let unwrap_y_fwd : result i32 = let w = y_c in Return w.wrap_val
+
+(** [constants::YVAL] *)
+let yval_body : result i32 =
+ begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end
+let yval_c : i32 = eval_global yval_body
+
+(** [constants::get_z1::Z1] *)
+let get_z1_z1_body : result i32 = Return 3
+let get_z1_z1_c : i32 = eval_global get_z1_z1_body
+
+(** [constants::get_z1] *)
+let get_z1_fwd : result i32 = let i = get_z1_z1_c in Return i
+
+(** [constants::add] *)
+let add_fwd (a : i32) (b : i32) : result i32 =
+ begin match i32_add a b with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::Q1] *)
+let q1_body : result i32 = Return 5
+let q1_c : i32 = eval_global q1_body
+
+(** [constants::Q2] *)
+let q2_body : result i32 = let i = q1_c in Return i
+let q2_c : i32 = eval_global q2_body
+
+(** [constants::Q3] *)
+let q3_body : result i32 =
+ let i = q2_c in
+ begin match add_fwd i 3 with | Fail -> Fail | Return i0 -> Return i0 end
+let q3_c : i32 = eval_global q3_body
+
+(** [constants::get_z2] *)
+let get_z2_fwd : result i32 =
+ begin match get_z1_fwd with
+ | Fail -> Fail
+ | Return i ->
+ let i0 = q3_c in
+ begin match add_fwd i i0 with
+ | Fail -> Fail
+ | Return i1 ->
+ let i2 = q1_c in
+ begin match add_fwd i2 i1 with
+ | Fail -> Fail
+ | Return i3 -> Return i3
+ end
+ end
+ end
+
+(** [constants::S1] *)
+let s1_body : result u32 = Return 6
+let s1_c : u32 = eval_global s1_body
+
+(** [constants::S2] *)
+let s2_body : result u32 =
+ let i = s1_c in
+ begin match incr_fwd i with | Fail -> Fail | Return i0 -> Return i0 end
+let s2_c : u32 = eval_global s2_body
+
+(** [constants::S3] *)
+let s3_body : result (pair_t u32 u32) = let p = p3_c in Return p
+let s3_c : pair_t u32 u32 = eval_global s3_body
+
+(** [constants::S4] *)
+let s4_body : result (pair_t u32 u32) =
+ begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end
+let s4_c : pair_t u32 u32 = eval_global s4_body
+
diff --git a/tests/misc/Makefile b/tests/misc/Makefile
index 5153d201..ea838d2d 100644
--- a/tests/misc/Makefile
+++ b/tests/misc/Makefile
@@ -1,2 +1,48 @@
-%.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)) > $@
+
+.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/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index 35d32514..a694cff1 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -218,36 +218,36 @@ let _ = assert_norm (get_elem_test_fwd = Return ())
(** [no_nested_borrows::test_char] *)
let test_char_fwd : result char = Return 'a'
-(** [no_nested_borrows::Tree] *)
-type tree_t (t : Type0) =
-| TreeLeaf : t -> tree_t t
-| TreeNode : t -> node_elem_t t -> tree_t t -> tree_t t
-
(** [no_nested_borrows::NodeElem] *)
-and node_elem_t (t : Type0) =
+type node_elem_t (t : Type0) =
| NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t
| NodeElemNil : node_elem_t t
-(** [no_nested_borrows::even] *)
-let rec even_fwd (x : u32) : result bool =
+(** [no_nested_borrows::Tree] *)
+and tree_t (t : Type0) =
+| TreeLeaf : t -> tree_t t
+| TreeNode : t -> node_elem_t t -> tree_t t -> tree_t t
+
+(** [no_nested_borrows::odd] *)
+let rec odd_fwd (x : u32) : result bool =
if x = 0
- then Return true
+ then Return false
else
begin match u32_sub x 1 with
| Fail -> Fail
| Return i ->
- begin match odd_fwd i with | Fail -> Fail | Return b -> Return b end
+ begin match even_fwd i with | Fail -> Fail | Return b -> Return b end
end
-(** [no_nested_borrows::odd] *)
-and odd_fwd (x : u32) : result bool =
+(** [no_nested_borrows::even] *)
+and even_fwd (x : u32) : result bool =
if x = 0
- then Return false
+ then Return true
else
begin match u32_sub x 1 with
| Fail -> Fail
| Return i ->
- begin match even_fwd i with | Fail -> Fail | Return b -> Return b end
+ begin match odd_fwd i with | Fail -> Fail | Return b -> Return b end
end
(** [no_nested_borrows::test_even_odd] *)