diff options
| author | Sidney Congard | 2022-06-30 14:54:15 +0200 |
|---|---|---|
| committer | Sidney Congard | 2022-06-30 14:54:15 +0200 |
| commit | fdbbb82ff89b1d5141ec63bc2385936da3de3616 (patch) | |
| tree | d48e3fa933280e8a275d2cfdab8f126e920e5f13 | |
| parent | 47691de8fe3dc32a29663d4d8343eb415ce1d81e (diff) | |
| parent | 4f33892c81cdaf6aefaad9b7cef1456dcfead67c (diff) | |
Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2
Complete the constants extraction by making all functions fail
30 files changed, 790 insertions, 420 deletions
@@ -31,6 +31,10 @@ _opam/ # Rust working directory rust-tests/target/ +# F* +.depend +*.hints + # Misc /fstar-tests *~ @@ -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 @@ -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. @@ -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] *) |