summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-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
14 files changed, 328 insertions, 178 deletions
diff --git a/src/Cps.ml b/src/Cps.ml
index d7c50f26..2d7dd2be 100644
--- a/src/Cps.ml
+++ b/src/Cps.ml
@@ -77,7 +77,6 @@ let comp_ret_val (f : (V.typed_value -> m_fun) -> m_fun)
comp f g
let apply (f : cm_fun) (g : m_fun) : m_fun = fun ctx -> f g ctx
-
let id_cm_fun : cm_fun = fun cf ctx -> cf ctx
(** If we have a list of [inputs] of type `'a list` and a function [f] which
@@ -92,7 +91,37 @@ let id_cm_fun : cm_fun = fun cf ctx -> cf ctx
See the unit test below for an illustration.
*)
-let fold_left_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd)
+let fold_left_apply_continuation (f : 'a -> ('c -> 'd) -> 'c -> 'd)
+ (inputs : 'a list) (cf : 'c -> 'd) : 'c -> 'd =
+ let rec eval_list (inputs : 'a list) (cf : 'c -> 'd) : 'c -> 'd =
+ fun ctx ->
+ match inputs with
+ | [] -> cf ctx
+ | x :: inputs -> comp (f x) (fun cf -> eval_list inputs cf) cf ctx
+ in
+ eval_list inputs cf
+
+(** Unit test/example for [fold_left_apply_continuation] *)
+let _ =
+ fold_left_apply_continuation
+ (fun x cf (ctx : int) -> cf (ctx + x))
+ [ 1; 20; 300; 4000 ]
+ (fun (ctx : int) -> assert (ctx = 4321))
+ 0
+
+(** If we have a list of [inputs] of type `'a list` and a function [f] which
+ evaluates one element of type `'a` to compute a result of type `'b` before
+ giving it to a continuation, the following function performs a fold operation:
+ it evaluates all the inputs one by one by accumulating the results in a list,
+ and gives the list to a continuation.
+
+ Note that we make sure that the results are listed in the order in
+ which they were computed (the first element of the list is the result
+ of applying [f] to the first element of the inputs).
+
+ See the unit test below for an illustration.
+ *)
+let fold_left_list_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd)
(inputs : 'a list) (cf : 'b list -> 'c -> 'd) : 'c -> 'd =
let rec eval_list (inputs : 'a list) (cf : 'b list -> 'c -> 'd)
(outputs : 'b list) : 'c -> 'd =
@@ -104,9 +133,9 @@ let fold_left_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd)
in
eval_list inputs cf []
-(** Unit test/example for [fold_left_apply_continuation] *)
+(** Unit test/example for [fold_left_list_apply_continuation] *)
let _ =
- fold_left_apply_continuation
+ fold_left_list_apply_continuation
(fun x cf (ctx : unit) -> cf (10 + x) ctx)
[ 0; 1; 2; 3; 4 ]
(fun values _ctx -> assert (values = [ 10; 11; 12; 13; 14 ]))
diff --git a/src/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. *)
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-05 22:17:25 +0000