summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-29 17:00:46 +0100
committerSon Ho2021-11-29 17:00:46 +0100
commit30628d4bbc3ea8a4b2e716d5c83323599ed98cce (patch)
tree64bbd82258afb1353f33b48abf1a4b6b528f5af4
parent18298def3e1bda9c5db907d4b0432557a76df337 (diff)
Start working logging and make progress on printing ASTs
Diffstat (limited to '')
-rw-r--r--src/Contexts.ml2
-rw-r--r--src/Identifiers.ml2
-rw-r--r--src/Interpreter.ml1
-rw-r--r--src/Logging.ml3
-rw-r--r--src/Print.ml179
-rw-r--r--src/Substitute.ml2
-rw-r--r--src/Types.ml7
-rw-r--r--src/dune2
-rw-r--r--src/main.ml2
9 files changed, 188 insertions, 12 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml
index f13043d0..b18cfe22 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -1,8 +1,6 @@
open Types
open Values
-open Expressions
open CfimAst
-open Errors
(** Environment value: mapping from variable to value, abstraction (only
used in symbolic mode) or stack frame delimiter.
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 8072b316..b858360d 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -1,5 +1,3 @@
-open Errors
-
(** Signature for a module describing an identifier.
We often need identifiers (for definitions, variables, etc.) and in
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 07c43c10..47b389a3 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -6,6 +6,7 @@ open Errors
module C = Contexts
module Subst = Substitute
module A = CfimAst
+module L = Logging
(* TODO: Change state-passing style to : st -> ... -> (st, v) *)
(* TODO: check that the value types are correct when evaluating *)
diff --git a/src/Logging.ml b/src/Logging.ml
new file mode 100644
index 00000000..b1512af7
--- /dev/null
+++ b/src/Logging.ml
@@ -0,0 +1,3 @@
+let _ = Easy_logging.Logging.make_logger "MainLogger" Debug [ Cli Debug ]
+
+let log = Easy_logging.Logging.get_logger "MainLogger"
diff --git a/src/Print.ml b/src/Print.ml
index 8d3e8745..9c9a7a5b 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -1,5 +1,8 @@
-open Errors
+(* TODO: use one letter abbreviations for modules *)
+
open Identifiers
+module T = Types
+module V = Values
open Types
(** Pretty-printing for types *)
@@ -73,7 +76,8 @@ module Types = struct
let params = params_to_string fmt regions tys in
match aty with Box -> "std::boxed::Box" ^ params)
- and params_to_string fmt (regions : 'r list) (types : 'r ty list) : string =
+ and params_to_string (fmt : 'r type_formatter) (regions : 'r list)
+ (types : 'r ty list) : string =
if List.length regions + List.length types > 0 then
let regions = List.map fmt.r_to_string regions in
let types = List.map (ty_to_string fmt) types in
@@ -145,6 +149,7 @@ end
(** Pretty-printing for values *)
open Values
+module PT = Types (* local module *)
module Values = struct
open Types (* local module *)
@@ -159,7 +164,7 @@ module Values = struct
let value_to_etype_formatter (fmt : value_formatter) : etype_formatter =
{
- Types.r_to_string = erased_region_to_string;
+ Types.r_to_string = PT.erased_region_to_string;
Types.type_var_id_to_string = fmt.type_var_id_to_string;
Types.type_def_id_to_string = fmt.type_def_id_to_string;
}
@@ -465,3 +470,171 @@ module Contexts = struct
in
"# " ^ string_of_int num_frames ^ " frame(s)\n" ^ String.concat "" frames
end
+
+module E = Expressions
+module A = CfimAst
+
+module CfimAst = struct
+ module PV = Values
+ module PC = Contexts
+ module PT = Types
+
+ type ast_formatter = {
+ r_to_string : RegionVarId.id -> string;
+ type_var_id_to_string : TypeVarId.id -> string;
+ type_def_id_to_string : TypeDefId.id -> string;
+ (* TODO: rename to something like adt_variant_to_string *)
+ type_def_id_variant_id_to_string : TypeDefId.id -> VariantId.id -> string;
+ adt_field_to_string :
+ TypeDefId.id -> VariantId.id option -> FieldId.id -> string;
+ var_id_to_string : VarId.id -> string;
+ fun_def_id_to_string : A.FunDefId.id -> string;
+ }
+
+ let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter =
+ {
+ PV.r_to_string = fmt.r_to_string;
+ PV.type_var_id_to_string = fmt.type_var_id_to_string;
+ PV.type_def_id_to_string = fmt.type_def_id_to_string;
+ PV.type_def_id_variant_id_to_string = fmt.type_def_id_variant_id_to_string;
+ PV.var_id_to_string = fmt.var_id_to_string;
+ }
+
+ let ast_to_etype_formatter (fmt : ast_formatter) : PT.etype_formatter =
+ {
+ PT.r_to_string = PT.erased_region_to_string;
+ PT.type_var_id_to_string = fmt.type_var_id_to_string;
+ PT.type_def_id_to_string = fmt.type_def_id_to_string;
+ }
+
+ let rec projection_to_string (fmt : ast_formatter) (inside : string)
+ (p : E.projection) : string =
+ match p with
+ | [] -> inside
+ | pe :: p' -> (
+ let s = projection_to_string fmt inside p' in
+ match pe with
+ | E.Deref -> "*(" ^ s ^ ")"
+ | E.DerefBox -> "deref_box(" ^ s ^ ")"
+ | E.Field (E.ProjTuple _, fid) -> "(" ^ s ^ ")." ^ FieldId.to_string fid
+ | E.Field (E.ProjAdt (adt_id, opt_variant_id), fid) -> (
+ let field_name =
+ fmt.adt_field_to_string adt_id opt_variant_id fid
+ in
+ match opt_variant_id with
+ | None -> "(" ^ s ^ ")." ^ field_name
+ | Some variant_id ->
+ let variant_name =
+ fmt.type_def_id_variant_id_to_string adt_id variant_id
+ in
+ "(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name))
+
+ let place_to_string (fmt : ast_formatter) (p : E.place) : string =
+ let var = fmt.var_id_to_string p.E.var_id in
+ projection_to_string fmt var p.E.projection
+
+ let unop_to_string (unop : E.unop) : string =
+ match unop with E.Not -> "¬" | E.Neg -> "-"
+
+ let binop_to_string (binop : E.binop) : string =
+ match binop with
+ | E.BitXor -> "^"
+ | E.BitAnd -> "&"
+ | E.BitOr -> "|"
+ | E.Eq -> "=="
+ | E.Lt -> "<"
+ | E.Le -> "<="
+ | E.Ne -> "!="
+ | E.Ge -> ">="
+ | E.Gt -> ">"
+ | E.Div -> "/"
+ | E.Rem -> "%"
+ | E.Add -> "+"
+ | E.Sub -> "-"
+ | E.Mul -> "*"
+ | E.Shl -> "<<"
+ | E.Shr -> ">>"
+
+ let operand_constant_value_to_string (fmt : ast_formatter)
+ (cv : E.operand_constant_value) : string =
+ match cv with
+ | E.ConstantValue cv -> PV.constant_value_to_string cv
+ | E.ConstantAdt def_id -> fmt.type_def_id_to_string def_id
+ | E.Unit -> "()"
+
+ let operand_to_string (fmt : ast_formatter) (op : E.operand) : string =
+ match op with
+ | E.Copy p -> "copy " ^ place_to_string fmt p
+ | E.Move p -> "move " ^ place_to_string fmt p
+ | E.Constant (_ty, cv) -> operand_constant_value_to_string fmt cv
+
+ let rvalue_to_string (fmt : ast_formatter) (rv : E.rvalue) : string =
+ match rv with
+ | E.Use op -> operand_to_string fmt op
+ | E.Ref (p, bk) -> (
+ let p = place_to_string fmt p in
+ match bk with
+ | E.Shared -> "&" ^ p
+ | E.Mut -> "&mut " ^ p
+ | E.TwoPhaseMut -> "&two-phase " ^ p)
+ | E.UnaryOp (unop, op) ->
+ unop_to_string unop ^ " " ^ operand_to_string fmt op
+ | E.BinaryOp (binop, op1, op2) ->
+ operand_to_string fmt op1 ^ " " ^ binop_to_string binop ^ " "
+ ^ operand_to_string fmt op2
+ | E.Discriminant p -> "discriminant(" ^ place_to_string fmt p ^ ")"
+ | E.Aggregate (akind, ops) -> (
+ let ops = List.map (operand_to_string fmt) ops in
+ match akind with
+ | E.AggregatedTuple -> "(" ^ String.concat ", " ops ^ ")"
+ | E.AggregatedAdt (def_id, opt_variant_id, _regions, _types) -> (
+ let adt_name = fmt.type_def_id_to_string def_id in
+ match opt_variant_id with
+ | None -> adt_name ^ "{ " ^ String.concat ", " ops ^ " }"
+ | Some variant_id ->
+ let variant_name =
+ fmt.type_def_id_variant_id_to_string def_id variant_id
+ in
+ adt_name ^ "::" ^ variant_name ^ "(" ^ String.concat ", " ops
+ ^ ")"))
+
+ let statement_to_string (fmt : ast_formatter) (st : A.statement) : string =
+ match st with
+ | A.Assign (p, rv) ->
+ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv
+ | A.FakeRead p -> "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 *)
+ "set_discriminant(" ^ place_to_string fmt p ^ ", "
+ ^ T.VariantId.to_string variant_id
+ ^ ")"
+ | A.Drop p -> "drop(" ^ place_to_string fmt p ^ ")"
+ | A.Assert a ->
+ let cond = operand_to_string fmt a.A.cond in
+ if a.A.expected then "assert(" ^ cond ^ ")"
+ else "assert(¬" ^ cond ^ ")"
+ | A.Call call -> (
+ let ty_fmt = ast_to_etype_formatter fmt in
+ let params =
+ if List.length call.A.type_params > 0 then
+ "<"
+ ^ String.concat ","
+ (List.map (PT.ty_to_string ty_fmt) call.A.type_params)
+ ^ ">"
+ else ""
+ in
+ match call.A.func with
+ | A.Local fid -> fmt.fun_def_id_to_string fid ^ params
+ | A.Assumed fid -> (
+ match fid with
+ | A.BoxNew -> "alloc::boxed::Box" ^ params ^ "::new"
+ | A.BoxDeref -> "core::ops::deref::Deref<Box" ^ params ^ ">::deref"
+ | A.BoxDerefMut ->
+ "core::ops::deref::DerefMut<Box" ^ params ^ ">::deref_mut"
+ | A.BoxFree -> "alloc::alloc::box_free<" ^ params ^ ">"))
+ | A.Panic -> "panic"
+ | A.Return -> "return"
+ | A.Break i -> "break " ^ string_of_int i
+ | A.Continue i -> "continue " ^ string_of_int i
+ | A.Nop -> "nop"
+end
diff --git a/src/Substitute.ml b/src/Substitute.ml
index dc2821f0..8cb92587 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -36,7 +36,7 @@ let rec ty_substitute (rsubst : 'r1 -> 'r2)
(** Erase the regions in a type and substitute the type variables *)
let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety)
(ty : T.rty) : T.ety =
- let rsubst (r : T.RegionVarId.id T.region) : T.erased_region = T.Erased in
+ let rsubst (_ : T.RegionVarId.id T.region) : T.erased_region = T.Erased in
ty_substitute rsubst tsubst ty
(** Create a type substitution from a list of type variable ids and a list of
diff --git a/src/Types.ml b/src/Types.ml
index 6f979718..abcd0e28 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -99,7 +99,10 @@ type type_def = {
kind : type_def_kind;
}
-(** Convert an [rty] to an [ety] by erasing the region variables *)
+(** Convert an [rty] to an [ety] by erasing the region variables
+
+ TODO: this can be done through a substitution
+*)
let rec erase_regions (ty : rty) : ety =
match ty with
| Adt (def_id, regions, tys) ->
@@ -115,7 +118,7 @@ let rec erase_regions (ty : rty) : ety =
| Str -> Str
| Array ty -> Array (erase_regions ty)
| Slice ty -> Slice (erase_regions ty)
- | Ref (r, ty, ref_kind) -> Ref (Erased, erase_regions ty, ref_kind)
+ | Ref (_, ty, ref_kind) -> Ref (Erased, erase_regions ty, ref_kind)
| Assumed (aty, regions, tys) ->
let regions = List.map (fun _ -> Erased) regions in
let tys = List.map erase_regions tys in
diff --git a/src/dune b/src/dune
index eb2966f4..c565d9fa 100644
--- a/src/dune
+++ b/src/dune
@@ -1,6 +1,6 @@
(executable
(name main)
- (libraries yojson zarith))
+ (libraries yojson zarith easy_logging))
(env
(dev (flags
diff --git a/src/main.ml b/src/main.ml
index 4fb91cea..8c05c33b 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,5 +1,5 @@
open CfimOfJson
-open Interpreter
+open Logging
open Print
(* This is necessary to have a backtrace when raising exceptions - for some