summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-23 14:02:14 +0100
committerSon Ho2021-11-23 14:02:14 +0100
commitb96bd19fe1ff22c2f1e03332468d4e6abb8a947e (patch)
tree00c889edf8bc828ef3c984c2fb2945239a5594b9
parentfcc3a467886e5c95b065b1fc4c27301fd62d7c21 (diff)
Implement formatting for eval_ctx
-rw-r--r--src/Contexts.ml42
-rw-r--r--src/Identifiers.ml8
-rw-r--r--src/Print.ml85
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