diff options
| -rw-r--r-- | src/CfimAst.ml | 18 | ||||
| -rw-r--r-- | src/Expressions.ml | 23 | ||||
| -rw-r--r-- | src/Identifiers.ml | 10 | ||||
| -rw-r--r-- | src/Types.ml | 28 | ||||
| -rw-r--r-- | src/Values.ml | 8 | ||||
| -rw-r--r-- | src/main.ml | 8 |
6 files changed, 53 insertions, 42 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml index 6b882edb..80165371 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -6,12 +6,12 @@ open Expressions module FunDefId = IdGen () type assumed_fun_id = BoxNew | BoxDeref | BoxDerefMut | BoxFree -[@@deriving of_yojson] +[@@deriving yojson] type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id -[@@deriving of_yojson] +[@@deriving yojson] -type assertion = { cond : operand; expected : bool } [@@deriving of_yojson] +type assertion = { cond : operand; expected : bool } [@@deriving yojson] type fun_sig = { region_params : region_var RegionVarId.vector; @@ -20,7 +20,7 @@ type fun_sig = { inputs : rty VarId.vector; output : rty; } -[@@deriving of_yojson] +[@@deriving yojson] type call = { func : fun_id; @@ -29,7 +29,7 @@ type call = { args : operand list; dest : place; } -[@@deriving of_yojson] +[@@deriving yojson] type statement = | Assign of place * rvalue @@ -50,14 +50,14 @@ type statement = (** Continue to (outer) loop. The loop identifier works the same way as for [Break] *) | Nop -[@@deriving of_yojson] +[@@deriving yojson] type expression = | Statement of statement | Sequence of expression * expression | Switch of operand * switch_targets | Loop of expression -[@@deriving of_yojson] +[@@deriving yojson] and switch_targets = | If of expression * expression (** Gives the "if" and "else" blocks *) @@ -67,7 +67,7 @@ and switch_targets = - the "otherwise" expression. Also note that we precise the type of the integer (uint32, int64, etc.) which we switch on. *) -[@@deriving of_yojson] +[@@deriving yojson] type fun_def = { def_id : FunDefId.id; @@ -78,4 +78,4 @@ type fun_def = { locals : var VarId.vector; body : expression; } -[@@deriving of_yojson] +[@@deriving yojson] diff --git a/src/Expressions.ml b/src/Expressions.ml index d8fe8d78..cd0a08ab 100644 --- a/src/Expressions.ml +++ b/src/Expressions.ml @@ -4,23 +4,22 @@ open Values type field_proj_kind = | Adt of TypeDefId.id * VariantId.id option | Tuple of int -[@@deriving of_yojson] +[@@deriving yojson] type projection_elem = | Deref | DerefBox | Field of field_proj_kind * FieldId.id | Downcast of VariantId.id -[@@deriving of_yojson] +[@@deriving yojson] -type projection = projection_elem list [@@deriving of_yojson] +type projection = projection_elem list [@@deriving yojson] -type place = { var_id : VarId.id; projection : projection } -[@@deriving of_yojson] +type place = { var_id : VarId.id; projection : projection } [@@deriving yojson] -type borrow_kind = Shared | Mut | TwoPhaseMut [@@deriving of_yojson] +type borrow_kind = Shared | Mut | TwoPhaseMut [@@deriving yojson] -type unop = Not | Neg [@@deriving of_yojson] +type unop = Not | Neg [@@deriving yojson] (** A binary operation @@ -46,7 +45,7 @@ type binop = | Mul | Shl | Shr -[@@deriving of_yojson] +[@@deriving yojson] (** Constant value for an operand @@ -65,16 +64,16 @@ type operand_constant_value = | ConstantValue of constant_value | Adt of TypeDefId.id | Unit -[@@deriving of_yojson] +[@@deriving yojson] type operand = | Copy of place | Move of place | Constant of ety * operand_constant_value -[@@deriving of_yojson] +[@@deriving yojson] type aggregate_kind = Tuple | Adt of TypeDefId.id * VariantId.id list -[@@deriving of_yojson] +[@@deriving yojson] type rvalue = | Use of operand @@ -83,4 +82,4 @@ type rvalue = | BinaryOp of binop * operand * operand | Discriminant of place | Aggregate of aggregate_kind * operand list -[@@deriving of_yojson] +[@@deriving yojson] diff --git a/src/Identifiers.ml b/src/Identifiers.ml index 51b6e473..27ed2921 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -19,11 +19,15 @@ module type Id = sig val id_of_yojson : Yojson.Safe.t -> (id, string) Result.result + val id_to_yojson : id -> Yojson.Safe.t + val vector_of_yojson : (Yojson.Safe.t -> ('a, string) Result.result) -> Yojson.Safe.t -> ('a vector, string) Result.result + val vector_to_yojson : ('a -> Yojson.Safe.t) -> 'a vector -> Yojson.Safe.t + (* TODO: remove *) (* module Map : Map.S with type key = id *) end @@ -34,9 +38,9 @@ end *) module IdGen () : Id = struct (* TODO: use Int64.t *) - type id = int [@@deriving of_yojson] + type id = int [@@deriving yojson] - type 'a vector = 'a list [@@deriving of_yojson] + type 'a vector = 'a list [@@deriving yojson] let zero = 0 @@ -73,6 +77,6 @@ module IdGen () : Id = struct module Map = Map.Make (ord) *) end -type name = string list [@@deriving of_yojson] +type name = string list [@@deriving yojson] (** A name such as: `std::collections::vector` (which would be represented as [["std"; "collections"; "vector"]]) *) diff --git a/src/Types.ml b/src/Types.ml index 16cb519d..c56f4b43 100644 --- a/src/Types.ml +++ b/src/Types.ml @@ -14,13 +14,13 @@ type type_var = { index : TypeVarId.id; (** Unique index identifying the variable *) name : string; (** Variable name *) } -[@@deriving of_yojson] +[@@deriving yojson] type region_var = { index : RegionVarId.id; (** Unique index identifying the region *) name : string option; (** Region name *) } -[@@deriving of_yojson] +[@@deriving yojson] (** A region. @@ -31,13 +31,13 @@ type region_var = { type 'rid region = | Static (** Static region *) | Var of 'rid (** Non-static region *) -[@@deriving of_yojson] +[@@deriving yojson] (** The type of erased regions. We could use unit, but having a dedicated type makes things more explicit. *) -type erased_region = Erased [@@deriving of_yojson] +type erased_region = Erased [@@deriving yojson] type integer_type = | Isize @@ -52,11 +52,11 @@ type integer_type = | U32 | U64 | U128 -[@@deriving of_yojson] +[@@deriving yojson] -type ref_kind = Mut | Shared [@@deriving of_yojson] +type ref_kind = Mut | Shared [@@deriving yojson] -type assumed_ty = Box [@@deriving of_yojson] +type assumed_ty = Box [@@deriving yojson] type 'r ty = | Adt of TypeDefId.id * 'r list * 'r ty list @@ -71,29 +71,29 @@ type 'r ty = | Ref of 'r * 'r ty * ref_kind | Tuple of 'r ty list | Assumed of assumed_ty * 'r list * 'r ty -[@@deriving of_yojson] +[@@deriving yojson] -type rty = RegionVarId.id region ty [@@deriving of_yojson] +type rty = RegionVarId.id region ty [@@deriving yojson] (** Type with *R*egions. Used in function signatures and type definitions. *) -type ety = erased_region ty [@@deriving of_yojson] +type ety = erased_region ty [@@deriving yojson] (** Type with *E*rased regions. Used in function bodies, "general" value types, etc. *) -type field = { name : string; ty : rty } [@@deriving of_yojson] +type field = { name : string; ty : rty } [@@deriving yojson] type variant = { name : string; fields : field FieldId.vector } -[@@deriving of_yojson] +[@@deriving yojson] type type_def_kind = | Struct of field FieldId.vector | Enum of variant VariantId.vector -[@@deriving of_yojson] +[@@deriving yojson] type type_def = { def_id : TypeDefId.id; @@ -102,4 +102,4 @@ type type_def = { type_params : type_var TypeVarId.vector; kind : type_def_kind; } -[@@deriving of_yojson] +[@@deriving yojson] diff --git a/src/Values.ml b/src/Values.ml index 992b43ea..ba5c7628 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -10,7 +10,7 @@ type var = { (** The variable type - erased type, because variables are not used ** in function signatures *) } -[@@deriving of_yojson] +[@@deriving yojson] (** A variable *) type big_int = Z.t @@ -21,6 +21,8 @@ let big_int_of_yojson (json : Yojson.Safe.t) : (big_int, string) result = | `Intlit is -> Ok (Z.of_string is) | _ -> Error "not an integer or an integer literal" +let big_int_to_yojson (i : big_int) = `Intlit (Z.to_string i) + (** A scalar value Note that we use unbounded integers everywhere. @@ -39,11 +41,11 @@ type scalar_value = | U32 of big_int | U64 of big_int | U128 of big_int -[@@deriving of_yojson] +[@@deriving yojson] type constant_value = | Scalar of scalar_value | Bool of bool | Char of char | String of string -[@@deriving of_yojson] +[@@deriving yojson] diff --git a/src/main.ml b/src/main.ml index fc9e4efd..ce0a9269 100644 --- a/src/main.ml +++ b/src/main.ml @@ -18,7 +18,13 @@ type rust_module = { let () = (* let json = Yojson.Basic.from_file "../charon/charon/tests/test1.cfim" in *) let _json1 = Yojson.Safe.from_file "../charon/charon/tests/test1.cfim" in - let json2 = Yojson.Safe.from_file "../charon/charon/tests/test4.cfim" in + let st1 = Return in + let json1 = statement_to_yojson st1 in + print_endline (Yojson.Safe.to_string json1); + let e1 = Statement Return in + let e1_json = expression_to_yojson e1 in + print_endline (Yojson.Safe.to_string e1_json); + let json2 = Yojson.Safe.from_string "[\"Return\"]" in match statement_of_yojson json2 with | Error s -> Printf.printf "error: %s\n" s | Ok _ast -> print_endline "ast" |