summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Expressions.ml78
-rw-r--r--src/Values.ml40
2 files changed, 118 insertions, 0 deletions
diff --git a/src/Expressions.ml b/src/Expressions.ml
new file mode 100644
index 00000000..f890f9c4
--- /dev/null
+++ b/src/Expressions.ml
@@ -0,0 +1,78 @@
+open Types
+open Values
+
+type field_proj_kind =
+ | Adt of TypeDefId.id * VariantId.id option
+ | Tuple of int
+
+type projection_elem =
+ | Deref
+ | DerefBox
+ | Field of field_proj_kind * FieldId.id
+ | Downcast of VariandId.id
+
+type projection = projection_elem list
+
+type place = { var_id : VarId.id; projection : projection }
+
+type borrow_kind = Shared | Mut | TwoPhaseMut
+
+type unop = Not | Neg
+
+(** A binary operation
+
+ Note that we merge checked binops and unchecked binops: we perform a
+ micro-pass on the MIR AST to remove the assertions introduced by rustc,
+ and use monadic functions for the binops which can fail (addition,
+ substraction, etc.) or have preconditions (division, remainder...)
+ *)
+type binop =
+ | BitXor
+ | BitAnd
+ | BitOr
+ | Eq
+ | Lt
+ | Le
+ | Ne
+ | Ge
+ | Gt
+ | Div
+ | Rem
+ | Add
+ | Sub
+ | Mul
+ | Shl
+ | Shr
+
+(** Constant value for an operand
+
+ It is a bit annoying, but Rust treats some ADT and tuple instances as
+ constants.
+ For instance, an enumeration with one variant and no fields is a constant.
+ A structure with no field is a constant.
+
+ For our translation, we use the following enumeration to encode those
+ special cases in assignments. They are converted to "normal" values
+ when evaluating the assignment (which is why we don't put them in the
+ [ConstantValue] enumeration.
+
+ *)
+type operand_constant_value =
+ | ConstantValue of constant_value
+ | Adt of TypeDefId.id
+ | Unit
+
+type operand =
+ | Copy of place
+ | Move of place
+ | Constant of ety * operand_constant_value
+
+type aggregate_kind = Tuple | Adt of TypeDefId.id * VariantId.id list
+
+type rvalue =
+ | Use of operand
+ | Ref of place * borrow_kind
+ | UnaryOp of unop * operand
+ | BinaryOp of binop * operand * operand
+ | Discriminant of place
+ | Aggregate of aggregate_kind * operand list
diff --git a/src/Values.ml b/src/Values.ml
new file mode 100644
index 00000000..006cc8da
--- /dev/null
+++ b/src/Values.ml
@@ -0,0 +1,40 @@
+open Identifiers
+open Types
+
+module VarId = IdGen ()
+
+module FunDefId = IdGen ()
+
+type var = {
+ index : VarId.id; (** Unique variable identifier *)
+ name : string option;
+ ty : ety;
+ (** The variable type - erased type, because variables are not used
+ ** in function signatures *)
+}
+(** A variable *)
+
+(** 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
+
+type constant_value =
+ | Scalar of scalar_value
+ | Bool of bool
+ | Char of char
+ | String of string