summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-17 14:26:43 +0100
committerSon Ho2021-11-17 14:26:43 +0100
commit7c62043ab195ee9844d29ade76efdf839a2e98d0 (patch)
treeaa0aa45d5d11da055604fe7ec503a907bc47af82
parent25fe1a81758bcf25171beee849467b2fff673b20 (diff)
Use [@@ëerive of_json] on all the types
-rw-r--r--src/CfimAst.ml10
-rw-r--r--src/Expressions.ml14
-rw-r--r--src/Identifiers.ml3
-rw-r--r--src/Types.ml20
-rw-r--r--src/Values.ml35
-rw-r--r--src/dune2
-rw-r--r--src/main.ml2
7 files changed, 61 insertions, 25 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 1fd8ccd4..66e3fb0c 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -4,10 +4,12 @@ open Values
open Expressions
type assumed_fun_id = BoxNew | BoxDeref | BoxDerefMut | BoxFree
+[@@deriving of_yojson]
type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id
+[@@deriving of_yojson]
-type assertion = { cond : operand; expected : bool }
+type assertion = { cond : operand; expected : bool } [@@deriving of_yojson]
type fun_sig = {
region_params : region_var RegionVarId.vector;
@@ -16,6 +18,7 @@ type fun_sig = {
inputs : rty VarId.vector;
output : rty;
}
+[@@deriving of_yojson]
type call = {
func : fun_id;
@@ -24,6 +27,7 @@ type call = {
args : operand list;
dest : place;
}
+[@@deriving of_yojson]
type statement =
| Assign of place * rvalue
@@ -44,12 +48,14 @@ type statement =
(** Continue to (outer) loop. The loop identifier works
the same way as for [Break] *)
| Nop
+[@@deriving of_yojson]
type expression =
| Statement of statement
| Sequence of expression * expression
| Switch of operand * switch_targets
| Loop of expression
+[@@deriving of_yojson]
and switch_targets =
| If of expression * expression (** Gives the "if" and "else" blocks *)
@@ -59,6 +65,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]
type fun_def = {
def_id : FunDefId.id;
@@ -69,3 +76,4 @@ type fun_def = {
locals : var VarId.vector;
body : expression;
}
+[@@deriving of_yojson]
diff --git a/src/Expressions.ml b/src/Expressions.ml
index 6eb5531b..d8fe8d78 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -4,20 +4,23 @@ open Values
type field_proj_kind =
| Adt of TypeDefId.id * VariantId.id option
| Tuple of int
+[@@deriving of_yojson]
type projection_elem =
| Deref
| DerefBox
| Field of field_proj_kind * FieldId.id
| Downcast of VariantId.id
+[@@deriving of_yojson]
-type projection = projection_elem list
+type projection = projection_elem list [@@deriving of_yojson]
type place = { var_id : VarId.id; projection : projection }
+[@@deriving of_yojson]
-type borrow_kind = Shared | Mut | TwoPhaseMut
+type borrow_kind = Shared | Mut | TwoPhaseMut [@@deriving of_yojson]
-type unop = Not | Neg
+type unop = Not | Neg [@@deriving of_yojson]
(** A binary operation
@@ -43,6 +46,7 @@ type binop =
| Mul
| Shl
| Shr
+[@@deriving of_yojson]
(** Constant value for an operand
@@ -61,13 +65,16 @@ type operand_constant_value =
| ConstantValue of constant_value
| Adt of TypeDefId.id
| Unit
+[@@deriving of_yojson]
type operand =
| Copy of place
| Move of place
| Constant of ety * operand_constant_value
+[@@deriving of_yojson]
type aggregate_kind = Tuple | Adt of TypeDefId.id * VariantId.id list
+[@@deriving of_yojson]
type rvalue =
| Use of operand
@@ -76,3 +83,4 @@ type rvalue =
| BinaryOp of binop * operand * operand
| Discriminant of place
| Aggregate of aggregate_kind * operand list
+[@@deriving of_yojson]
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 6140b7d4..51b6e473 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -33,6 +33,7 @@ end
See [Id].
*)
module IdGen () : Id = struct
+ (* TODO: use Int64.t *)
type id = int [@@deriving of_yojson]
type 'a vector = 'a list [@@deriving of_yojson]
@@ -72,6 +73,6 @@ module IdGen () : Id = struct
module Map = Map.Make (ord) *)
end
-type name = string list
+type name = string list [@@deriving of_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 d435863e..16cb519d 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -14,11 +14,13 @@ type type_var = {
index : TypeVarId.id; (** Unique index identifying the variable *)
name : string; (** Variable name *)
}
+[@@deriving of_yojson]
type region_var = {
index : RegionVarId.id; (** Unique index identifying the region *)
name : string option; (** Region name *)
}
+[@@deriving of_yojson]
(** A region.
@@ -29,12 +31,13 @@ type region_var = {
type 'rid region =
| Static (** Static region *)
| Var of 'rid (** Non-static region *)
+[@@deriving of_yojson]
(** The type of erased regions.
We could use unit, but having a dedicated type makes things more explicit.
*)
-type erased_region = Erased
+type erased_region = Erased [@@deriving of_yojson]
type integer_type =
| Isize
@@ -49,10 +52,11 @@ type integer_type =
| U32
| U64
| U128
+[@@deriving of_yojson]
-type ref_kind = Mut | Shared
+type ref_kind = Mut | Shared [@@deriving of_yojson]
-type assumed_ty = Box
+type assumed_ty = Box [@@deriving of_yojson]
type 'r ty =
| Adt of TypeDefId.id * 'r list * 'r ty list
@@ -67,26 +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]
-type rty = RegionVarId.id region ty
+type rty = RegionVarId.id region ty [@@deriving of_yojson]
(** Type with *R*egions.
Used in function signatures and type definitions.
*)
-type ety = erased_region ty
+type ety = erased_region ty [@@deriving of_yojson]
(** Type with *E*rased regions.
Used in function bodies, "general" value types, etc.
*)
-type field = { name : string; ty : rty }
+type field = { name : string; ty : rty } [@@deriving of_yojson]
type variant = { name : string; fields : field FieldId.vector }
+[@@deriving of_yojson]
type type_def_kind =
| Struct of field FieldId.vector
| Enum of variant VariantId.vector
+[@@deriving of_yojson]
type type_def = {
def_id : TypeDefId.id;
@@ -95,3 +102,4 @@ type type_def = {
type_params : type_var TypeVarId.vector;
kind : type_def_kind;
}
+[@@deriving of_yojson]
diff --git a/src/Values.ml b/src/Values.ml
index 006cc8da..bc917d85 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -12,29 +12,40 @@ type var = {
(** The variable type - erased type, because variables are not used
** in function signatures *)
}
+[@@deriving of_yojson]
(** A variable *)
+type big_int = Z.t
+
+let big_int_of_yojson (json : Yojson.Safe.t) : (big_int, string) result =
+ match json with
+ | `Int i -> Ok (Z.of_int i)
+ | `Intlit is -> Ok (Z.of_string is)
+ | _ -> Error "not an integer or an integer literal"
+
(** A scalar value
Note that we use unbounded integers everywhere.
We then harcode the boundaries for the different types.
*)
type scalar_value =
- | Isize of Big_int.big_int
- | I8 of Big_int.big_int
- | I16 of Big_int.big_int
- | I32 of Big_int.big_int
- | I64 of Big_int.big_int
- | I128 of Big_int.big_int
- | Usize of Big_int.big_int
- | U8 of Big_int.big_int
- | U16 of Big_int.big_int
- | U32 of Big_int.big_int
- | U64 of Big_int.big_int
- | U128 of Big_int.big_int
+ | Isize of big_int
+ | I8 of big_int
+ | I16 of big_int
+ | I32 of big_int
+ | I64 of big_int
+ | I128 of big_int
+ | Usize of big_int
+ | U8 of big_int
+ | U16 of big_int
+ | U32 of big_int
+ | U64 of big_int
+ | U128 of big_int
+[@@deriving of_yojson]
type constant_value =
| Scalar of scalar_value
| Bool of bool
| Char of char
| String of string
+[@@deriving of_yojson]
diff --git a/src/dune b/src/dune
index 2c07ec16..2611eb6e 100644
--- a/src/dune
+++ b/src/dune
@@ -1,4 +1,4 @@
(executable
(name main)
- (libraries yojson)
+ (libraries yojson zarith)
(preprocess (pps ppx_deriving.show ppx_deriving.ord ppx_deriving_yojson))) \ No newline at end of file
diff --git a/src/main.ml b/src/main.ml
index 3fd2a311..850c7bcf 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -25,5 +25,5 @@ type ty1 = int Id0.vector [@@deriving of_yojson]
let () =
(* let json = Yojson.Basic.from_file "../charon/charon/tests/test1.cfim" in *)
let _json = Yojson.Safe.from_file "../charon/charon/tests/test1.cfim" in
- let _test = ty1_of_yojson _json in
+ let _test = CfimAst.fun_def_of_yojson _json in
()