diff options
| -rw-r--r-- | src/Contexts.ml | 21 | ||||
| -rw-r--r-- | src/Interpreter.ml | 40 | ||||
| -rw-r--r-- | src/Print.ml | 45 | ||||
| -rw-r--r-- | src/Substitute.ml | 1 | ||||
| -rw-r--r-- | src/dune | 4 | ||||
| -rw-r--r-- | src/main.ml | 1 |
6 files changed, 61 insertions, 51 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index d576083d..25865064 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -4,7 +4,12 @@ open Expressions open CfimAst open Errors -type env_value = Var of var * typed_value | Abs of abs +(** Environment value: mapping from variable to value, abstraction (only + used in symbolic mode) or stack frame delimiter. + + TODO: rename? Environment element or something? + *) +type env_value = Var of var * typed_value | Abs of abs | Frame type env = env_value list @@ -12,19 +17,10 @@ type interpreter_mode = ConcreteMode | SymbolicMode type config = { mode : interpreter_mode; check_invariants : bool } -type stack_frame = { num_vars : int } -(** A function frame - - When using the interpreter in concrete mode (i.e, non symbolic) we - push a function frame whenever we enter a function body (and pop it - upon leaving it). - *) - type eval_ctx = { type_context : type_def TypeDefId.vector; fun_context : fun_def FunDefId.vector; type_vars : type_var TypeVarId.vector; - frames : stack_frame list; env : env; symbolic_counter : SymbolicValueId.generator; borrow_counter : BorrowId.generator; @@ -48,7 +44,7 @@ let ctx_lookup_var (ctx : eval_ctx) (vid : VarId.id) : var = | [] -> raise (Invalid_argument ("Variable not found: " ^ VarId.to_string vid)) | Var (var, _) :: env' -> if var.index = vid then var else lookup env' - | Abs _ :: env' -> lookup env' + | (Abs _ | Frame) :: env' -> lookup env' in lookup ctx.env @@ -63,7 +59,7 @@ let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = let check_ev (ev : env_value) : typed_value option = match ev with | Var (var, v) -> if var.index = vid then Some v else None - | Abs _ -> None + | Abs _ | Frame -> None in match List.find_map check_ev env with | None -> failwith "Unreachable" @@ -83,6 +79,7 @@ let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env = match ev with | Var (var, v) -> if var.index = vid then Var (var, nv) else Var (var, v) | Abs abs -> Abs abs + | Frame -> Frame in List.map update_ev env diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 60441ce7..9e109709 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -97,8 +97,8 @@ let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : let lookup_loan_in_env_value (ev : C.env_value) : V.loan_content option = match ev with | C.Var (_, v) -> lookup_loan_in_value ek l v - | C.Abs _ -> raise Unimplemented - (* TODO *) + | C.Abs _ -> raise Unimplemented (* TODO *) + | C.Frame -> None in match List.find_map lookup_loan_in_env_value env with | None -> failwith "Unreachable" @@ -158,8 +158,8 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id) let update_loan_in_env_value (ev : C.env_value) : C.env_value = match ev with | C.Var (vid, v) -> Var (vid, update_loan_in_value ek l nlc v) - | C.Abs _ -> raise Unimplemented - (* TODO *) + | C.Abs _ -> raise Unimplemented (* TODO *) + | C.Frame -> C.Frame in List.map update_loan_in_env_value env @@ -195,8 +195,8 @@ let lookup_borrow (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env) : let lookup_borrow_in_env_value (ev : C.env_value) = match ev with | C.Var (_, v) -> lookup_borrow_in_value ek l v - | C.Abs _ -> raise Unimplemented - (* TODO *) + | C.Abs _ -> raise Unimplemented (* TODO *) + | C.Frame -> None in match List.find_map lookup_borrow_in_env_value env with | None -> failwith "Unreachable" @@ -257,8 +257,8 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id) let update_borrow_in_env_value (ev : C.env_value) : C.env_value = match ev with | C.Var (vid, v) -> Var (vid, update_borrow_in_value ek l nbc v) - | C.Abs _ -> raise Unimplemented - (* TODO *) + | C.Abs _ -> raise Unimplemented (* TODO *) + | C.Frame -> C.Frame in List.map update_borrow_in_env_value env @@ -362,8 +362,9 @@ let rec bottom_in_value (v : V.typed_value) : bool = raise Unimplemented (** See [end_borrow_get_borrow_in_env] *) -let rec end_borrow_get_borrow_in_value config io l outer_borrows v0 : - V.typed_value * borrow_lres = +let rec end_borrow_get_borrow_in_value (config : C.config) (io : inner_outer) + (l : V.BorrowId.id) (outer_borrows : borrow_ids option) (v0 : V.typed_value) + : V.typed_value * borrow_lres = match v0.V.value with | V.Concrete _ | V.Bottom | V.Symbolic _ -> (v0, NotFound) | V.Assumed (Box bv) -> @@ -422,8 +423,9 @@ let rec end_borrow_get_borrow_in_value config io l outer_borrows v0 : in ({ v0 with value = V.Borrow (V.MutBorrow (l', bv')) }, res) -and end_borrow_get_borrow_in_values config io l outer_borrows vl0 : - V.typed_value list * borrow_lres = +and end_borrow_get_borrow_in_values (config : C.config) (io : inner_outer) + (l : V.BorrowId.id) (outer_borrows : borrow_ids option) + (vl0 : V.typed_value list) : V.typed_value list * borrow_lres = match vl0 with | [] -> (vl0, NotFound) | v :: vl -> ( @@ -447,8 +449,8 @@ and end_borrow_get_borrow_in_values config io l outer_borrows vl0 : borrows, we end them, and finally we end the borrow we wanted to end in the first place. *) -let rec end_borrow_get_borrow_in_env (config : C.config) (io : inner_outer) l - env0 : C.env * borrow_lres = +let rec end_borrow_get_borrow_in_env (config : C.config) (io : inner_outer) + (l : V.BorrowId.id) (env0 : C.env) : C.env * borrow_lres = match env0 with | [] -> ([], NotFound) | C.Var (x, v) :: env -> ( @@ -460,6 +462,7 @@ let rec end_borrow_get_borrow_in_env (config : C.config) (io : inner_outer) l | C.Abs _ :: _ -> assert (config.mode = SymbolicMode); raise Unimplemented + | C.Frame :: env -> end_borrow_get_borrow_in_env config io l env (** See [give_back_value]. *) let rec give_back_value_to_value config bid (v : V.typed_value) @@ -574,6 +577,9 @@ let give_back_shared_to_abs _config _bid _abs : V.abs = When we end a mutable borrow, we need to "give back" the value it contained to its original owner by reinserting it at the proper position. + + TODO: we must share that the borrow is somewhere in the environment, before + giving it back. *) let give_back_value (config : C.config) (bid : V.BorrowId.id) (v : V.typed_value) (env : C.env) : C.env = @@ -584,6 +590,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) | C.Abs abs -> assert (config.mode = SymbolicMode); C.Abs (give_back_value_to_abs config bid v abs) + | C.Frame -> C.Frame in List.map give_back_value_to_env_value env @@ -600,6 +607,7 @@ let give_back_shared config (bid : V.BorrowId.id) (env : C.env) : C.env = | C.Abs abs -> assert (config.mode = SymbolicMode); C.Abs (give_back_shared_to_abs config bid abs) + | C.Frame -> C.Frame in List.map give_back_shared_to_env_value env @@ -655,6 +663,7 @@ let reborrow_shared (config : C.config) (original_bid : V.BorrowId.id) | C.Abs abs -> assert (config.mode = SymbolicMode); C.Abs abs + | C.Frame -> C.Frame in List.map reborrow_in_ev env @@ -1500,6 +1509,8 @@ let prepare_rplace (config : C.config) (access : access_kind) (p : E.place) - [eval_operand_prepare] - [eval_operand_apply] which are then used in [eval_operand] and [eval_operands]. + + TODO: this is not the proper way of doing *) let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : C.eval_ctx = @@ -1895,6 +1906,7 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) : (C.eval_ctx * statement_eval_res) eval_result = match st with | A.Assign (p, rvalue) -> ( + (* TODO: this is WRONG *) (* Prepare the rvalue, prepare the destination *) let ctx1 = eval_rvalue_prepare config ctx rvalue in let ctx2, _ = prepare_lplace config p ctx1 in diff --git a/src/Print.ml b/src/Print.ml index 156c9fe1..8d3e8745 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -394,9 +394,9 @@ module Contexts = struct let env_value_to_string (fmt : value_formatter) (ev : env_value) : string = match ev with - | Var (vid, tv) -> - var_id_to_string vid ^ " -> " ^ typed_value_to_string fmt tv + | Var (var, tv) -> var_to_string var ^ " -> " ^ typed_value_to_string fmt tv | Abs abs -> abs_to_string fmt abs + | Frame -> failwith "Can't print a Frame element" let env_to_string (fmt : value_formatter) (env : env) : string = "{\n" @@ -426,8 +426,8 @@ module Contexts = struct Types.name_to_string def.name ^ "::" ^ variant.variant_name in let var_id_to_string vid = - let v = VarId.Map.find vid ctx.vars in - var_to_string v + let var = ctx_lookup_var ctx vid in + var_to_string var in { r_to_string; @@ -437,32 +437,31 @@ module Contexts = struct var_id_to_string; } - let frame_to_string (fmt : ctx_formatter) (ctx : eval_ctx) - (frame : stack_frame) : string = - let var_binding_to_string (vid : VarId.id) : string = - let var = ctx_lookup_var ctx vid in - let v = ctx_lookup_var_value ctx vid in - let var_name = - match var.name with Some name -> "(" ^ name ^ ")" | None -> "" - in - " @" ^ VarId.to_string var.index ^ var_name ^ " --> " - ^ typed_value_to_string fmt v - in - let vars = - String.concat ",\n" (List.map var_binding_to_string frame.vars) + (** Split an [env] at every occurrence of [Frame], eliminating those elements. + Also reorders the frames and the values in the frames according to the + following order: + * frames: from the first pushed (oldest) to the last pushed (current frame) + * values: from the first pushed (oldest) to the last pushed + *) + let split_env_according_to_frames (env : env) : env list = + let rec split_aux (frames : env list) (curr_frame : env) (env : env) = + match env with + | [] -> frames + | Frame :: env' -> split_aux (curr_frame :: frames) [] env' + | ev :: env' -> split_aux frames (ev :: curr_frame) env' in - "[\n" ^ vars ^ "\n]" + let frames = split_aux [] [] env in + List.rev frames let eval_ctx_to_string (ctx : eval_ctx) : string = let fmt = eval_ctx_to_ctx_formatter ctx in - let num_frames = List.length ctx.frames in + let frames = split_env_according_to_frames ctx.env in + let num_frames = List.length frames in let frames = List.mapi (fun i f -> - "\n# Frame " ^ string_of_int i ^ ":\n" ^ frame_to_string fmt ctx f - ^ "\n") - ctx.frames + "\n# Frame " ^ string_of_int i ^ ":\n" ^ env_to_string fmt f ^ "\n") + frames in - let frames = List.rev frames in "# " ^ string_of_int num_frames ^ " frame(s)\n" ^ String.concat "" frames end diff --git a/src/Substitute.ml b/src/Substitute.ml index fa7016b1..dc2821f0 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -31,6 +31,7 @@ let rec ty_substitute (rsubst : 'r1 -> 'r2) | Never -> Never | Integer int_ty -> Integer int_ty | Str -> Str + | TypeVar vid -> tsubst vid (** Erase the regions in a type and substitute the type variables *) let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety) @@ -7,11 +7,11 @@ :standard -safe-string -g - -warn-error -8-9-11-33-20-21-26-27-39 + -warn-error -9-11-33-20-21-26-27-39 )) (release (flags :standard -safe-string -g - -warn-error -8-9-11-33-20-21-26-27-39 + -warn-error -9-11-33-20-21-26-27-39 ))) diff --git a/src/main.ml b/src/main.ml index 46a8b678..4fb91cea 100644 --- a/src/main.ml +++ b/src/main.ml @@ -1,5 +1,6 @@ open CfimOfJson open Interpreter +open Print (* This is necessary to have a backtrace when raising exceptions - for some * reason, the -g option doesn't work *) |