summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Identifiers.ml4
-rw-r--r--src/Interpreter.ml26
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
- *)