diff options
author | Son Ho | 2023-12-14 17:11:54 +0100 |
---|---|---|
committer | Son Ho | 2023-12-14 17:11:54 +0100 |
commit | f074320eee2203857e669cfb72f7f8f94ab52151 (patch) | |
tree | d5f2f8d4a45f206e0a94e980ea4c6ad074f2bc19 /compiler/InterpreterExpressions.ml | |
parent | f69ac6a4a244c99a41a90ed57f74ea83b3835882 (diff) | |
parent | c3e0b90e422cbd902ee6d2b47073940c0017b7fb (diff) |
Merge remote-tracking branch 'origin/main' into son/merge_back
Diffstat (limited to 'compiler/InterpreterExpressions.ml')
-rw-r--r-- | compiler/InterpreterExpressions.ml | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 9f117933..1b5b79dd 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -435,7 +435,9 @@ let eval_unary_op_concrete (config : config) (unop : unop) (op : operand) match mk_scalar sv.int_ty i with | Error _ -> cf (Error EPanic) | Ok sv -> cf (Ok { v with value = VLiteral (VScalar sv) })) - | Cast (CastInteger (src_ty, tgt_ty)), VLiteral (VScalar sv) -> ( + | ( Cast (CastScalar (TInteger src_ty, TInteger tgt_ty)), + VLiteral (VScalar sv) ) -> ( + (* Cast between integers *) assert (src_ty = sv.int_ty); let i = sv.value in match mk_scalar tgt_ty i with @@ -444,6 +446,25 @@ let eval_unary_op_concrete (config : config) (unop : unop) (op : operand) let ty = TLiteral (TInteger tgt_ty) in let value = VLiteral (VScalar sv) in cf (Ok { ty; value })) + | Cast (CastScalar (TBool, TInteger tgt_ty)), VLiteral (VBool sv) -> ( + (* Cast bool -> int *) + let i = Z.of_int (if sv then 1 else 0) in + match mk_scalar tgt_ty i with + | Error _ -> cf (Error EPanic) + | Ok sv -> + let ty = TLiteral (TInteger tgt_ty) in + let value = VLiteral (VScalar sv) in + cf (Ok { ty; value })) + | Cast (CastScalar (TInteger _, TBool)), VLiteral (VScalar sv) -> + (* Cast int -> bool *) + let b = + if Z.of_int 0 = sv.value then false + else if Z.of_int 1 = sv.value then true + else raise (Failure "Conversion from int to bool: out of range") + in + let value = VLiteral (VBool b) in + let ty = TLiteral TBool in + cf (Ok { ty; value }) | _ -> raise (Failure "Invalid input for unop") in comp eval_op apply cf @@ -461,7 +482,7 @@ let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand) match (unop, v.ty) with | Not, (TLiteral TBool as lty) -> lty | Neg, (TLiteral (TInteger _) as lty) -> lty - | Cast (CastInteger (_, tgt_ty)), _ -> TLiteral (TInteger tgt_ty) + | Cast (CastScalar (_, tgt_ty)), _ -> TLiteral tgt_ty | _ -> raise (Failure "Invalid input for unop") in let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in |