From d7981190632dcac8e5579e41252ed47e2e5b0879 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 3 Nov 2021 12:38:52 +0100 Subject: Add Values.ml and Expressions.ml --- src/Expressions.ml | 78 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 78 insertions(+) create mode 100644 src/Expressions.ml (limited to 'src/Expressions.ml') 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 -- cgit v1.2.3