diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Contexts.ml | 42 | ||||
| -rw-r--r-- | src/Identifiers.ml | 8 | ||||
| -rw-r--r-- | src/Print.ml | 85 |
3 files changed, 119 insertions, 16 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index be8e56fa..88af46d4 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -2,25 +2,12 @@ open Types open Values open Expressions open CfimAst -open Print.Values open Errors type env_value = Var of VarId.id * typed_value | Abs of abs type env = env_value list -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 - | Abs abs -> abs_to_string fmt abs - -let env_to_string (fmt : value_formatter) (env : env) : string = - "{\n" - ^ String.concat ";\n" - (List.map (fun ev -> " " ^ env_value_to_string fmt ev) env) - ^ "\n}" - type 'a eval_result = Stuck | Panic | Res of 'a type interpreter_mode = ConcreteMode | SymbolicMode @@ -29,7 +16,7 @@ type config = { mode : interpreter_mode; check_invariants : bool } type outer_borrows = Borrows of BorrowId.Set.t | Borrow of BorrowId.id -type stack_frame = { vars : var VarId.vector } +type stack_frame = { vars : VarId.id list } (** A function frame When using the interpreter in concrete mode (i.e, non symbolic) we @@ -41,9 +28,34 @@ type eval_ctx = { type_context : type_def TypeDefId.vector; fun_context : fun_def FunDefId.vector; type_vars : type_var TypeVarId.vector; + vars : var VarId.Map.t; frames : stack_frame list; env : env; symbolic_counter : SymbolicValueId.generator; - borrows_counter : BorrowId.generator; + borrow_counter : BorrowId.generator; } (** Evaluation context *) + +let fresh_symbolic_value_id (ctx : eval_ctx) : SymbolicValueId.id * eval_ctx = + let id, counter' = SymbolicValueId.fresh ctx.symbolic_counter in + (id, { ctx with symbolic_counter = counter' }) + +let fresh_borrow_id (ctx : eval_ctx) : BorrowId.id * eval_ctx = + let id, counter' = BorrowId.fresh ctx.borrow_counter in + (id, { ctx with borrow_counter = counter' }) + +let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var = + TypeVarId.nth ctx.type_vars vid + +let lookup_var (ctx : eval_ctx) (vid : VarId.id) : var = + VarId.Map.find vid ctx.vars + +let lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value = + let check_ev (ev : env_value) : typed_value option = + match ev with + | Var (vid', v) -> if vid' = vid then Some v else None + | Abs _ -> None + in + match List.find_map check_ev ctx.env with + | None -> failwith "Unreachable" + | Some v -> v diff --git a/src/Identifiers.ml b/src/Identifiers.ml index cab1bafa..f01d4f47 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -40,6 +40,8 @@ module type Id = sig val set_to_string : Set.t -> string + module Map : Map.S with type key = id + val id_of_json : Yojson.Basic.t -> (id, string) result val vector_of_json : @@ -98,6 +100,12 @@ module IdGen () : Id = struct let compare = compare end) + module Map = Map.Make (struct + type t = id + + let compare = compare + end) + let set_to_string ids = let ids = Set.fold (fun id ids -> to_string id :: ids) ids [] in "{" ^ String.concat ", " (List.rev ids) ^ "}" diff --git a/src/Print.ml b/src/Print.ml index c8296754..ea368bd3 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -147,7 +147,7 @@ end open Values module Values = struct - open Types + open Types (* local module *) type value_formatter = { r_to_string : RegionVarId.id -> string; @@ -395,3 +395,86 @@ module Values = struct ^ RegionId.set_to_string abs.regions ^ "}" ^ " {\n" ^ avs ^ "\n}" end + +open Contexts +(** Pretty-printing for contexts *) + +module Contexts = struct + open Values (* local module *) + + open Contexts + + 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 + | Abs abs -> abs_to_string fmt abs + + let env_to_string (fmt : value_formatter) (env : env) : string = + "{\n" + ^ String.concat ";\n" + (List.map (fun ev -> " " ^ env_value_to_string fmt ev) env) + ^ "\n}" + + type ctx_formatter = value_formatter + + let eval_ctx_to_ctx_formatter (ctx : eval_ctx) : ctx_formatter = + (* We shouldn't use r_to_string *) + let r_to_string _ = failwith "Unreachable" in + let type_var_id_to_string vid = + let v = lookup_type_var ctx vid in + v.tv_name + in + let type_def_id_to_string def_id = + let def = TypeDefId.nth ctx.type_context def_id in + Types.name_to_string def.name + in + let type_def_id_variant_id_to_string def_id variant_id = + let def = TypeDefId.nth ctx.type_context def_id in + match def.kind with + | Struct _ -> failwith "Unreachable" + | Enum variants -> + let variant = VariantId.nth variants variant_id in + 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 + in + { + r_to_string; + type_var_id_to_string; + type_def_id_to_string; + type_def_id_variant_id_to_string; + 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 = lookup_var ctx vid in + let v = 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) + in + "[\n" ^ vars ^ "\n]" + + 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 = + List.mapi + (fun i f -> + "\n# Frame " ^ string_of_int i ^ ":\n" ^ frame_to_string fmt ctx f + ^ "\n") + ctx.frames + in + let frames = List.rev frames in + "# " ^ string_of_int num_frames ^ " frame(s)\n" ^ String.concat "" frames +end |