diff options
-rw-r--r-- | src/Expressions.ml | 78 | ||||
-rw-r--r-- | src/Values.ml | 40 |
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 |