diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Identifiers.ml | 4 | ||||
| -rw-r--r-- | src/Interpreter.ml | 26 |
2 files changed, 25 insertions, 5 deletions
diff --git a/src/Identifiers.ml b/src/Identifiers.ml index 22b52119..6f74e062 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -20,6 +20,8 @@ module type Id = sig val to_string : id -> string + val to_int : id -> int + val empty_vector : 'a vector val vector_to_list : 'a vector -> 'a list @@ -80,6 +82,8 @@ module IdGen () : Id = struct let to_string = string_of_int + let to_int x = x + let empty_vector = [] let vector_to_list v = v diff --git a/src/Interpreter.ml b/src/Interpreter.ml index ebb4f2ee..5c5a9617 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1640,9 +1640,25 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) : Ok ({ ctx3 with env = env4 }, rv)) | UnaryOp (unop, op) -> eval_unary_op config ctx unop op | BinaryOp (binop, op1, op2) -> eval_binary_op config ctx binop op1 op2 - | Discriminant p -> raise Unimplemented + | Discriminant p -> ( + (* Note that discriminant values have type `isize` *) + (* Access the value *) + let access = Read in + let ctx1, v = prepare_rplace config access p ctx in + match v.value with + | Adt av -> ( + match av.variant_id with + | None -> + failwith + "Invalid input for `discriminant`: structure instead of enum" + | Some variant_id -> ( + let id = Z.of_int (VariantId.to_int variant_id) in + match mk_scalar Isize id with + | Error _ -> + failwith "Disciminant id out of range" + (* Should really never happen *) + | Ok sv -> + Ok (ctx1, { value = Concrete (Scalar sv); ty = Integer Isize }) + )) + | _ -> failwith "Invalid input for `discriminant`") | Aggregate (aggregate_kind, ops) -> raise Unimplemented - -(* TODO: - update write_value - *) |