summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-20 00:29:04 +0100
committerSon Ho2022-01-20 00:29:04 +0100
commit15201d05ab21baa67191d6f5c4c6b54effef6642 (patch)
treeb4d7d7d34aa5f281e70ac00fbe60b2c8c0e6dc72
parentd371a3b7dc232311f1866ebf297d92021ec6d05b (diff)
Make more progress on InterpreterExpressions
-rw-r--r--src/InterpreterExpressions.ml215
1 files changed, 116 insertions, 99 deletions
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 4f4cf4e5..e80232c2 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -301,11 +301,12 @@ let eval_unary_op (config : C.config) (unop : E.unop) (op : E.operand)
| C.ConcreteMode -> eval_unary_op_concrete config unop op cf
| C.SymbolicMode -> eval_unary_op_symbolic config unop op cf
-let eval_binary_op_concrete (config : C.config) (binop : E.binop)
- (op1 : E.operand) (op2 : E.operand)
- (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
- (* Evaluate the operands *)
- let ctx, v1, v2 = eval_two_operands config ctx op1 op2 in
+(** Small helper for [eval_binary_op_concrete]: computes the result of applying
+ the binop *after* the operands have been successfully evaluated
+ *)
+let eval_binary_op_concrete_compute (config : C.config) (binop : E.binop)
+ (v1 : V.typed_value) (v2 : V.typed_value) :
+ (V.typed_value, eval_error) result =
(* Equality check binops (Eq, Ne) accept values from a wide variety of types.
* The remaining binops only operate on scalars. *)
if binop = Eq || binop = Ne then (
@@ -314,112 +315,128 @@ let eval_binary_op_concrete (config : C.config) (binop : E.binop)
(* Equality/inequality check is primitive only for a subset of types *)
assert (ty_is_primitively_copyable v1.ty);
let b = v1 = v2 in
- Ok (ctx, { V.value = V.Concrete (Bool b); ty = T.Bool }))
+ Ok { V.value = V.Concrete (Bool b); ty = T.Bool })
else
(* For the non-equality operations, the input values are necessarily scalars *)
match (v1.V.value, v2.V.value) with
| V.Concrete (V.Scalar sv1), V.Concrete (V.Scalar sv2) -> (
- let res =
- (* There are binops which require the two operands to have the same
- type, and binops for which it is not the case.
- There are also binops which return booleans, and binops which
- return integers.
- *)
- match binop with
- | E.Lt | E.Le | E.Ge | E.Gt ->
- (* The two operands must have the same type and the result is a boolean *)
- assert (sv1.int_ty = sv2.int_ty);
- let b =
- match binop with
- | E.Lt -> Z.lt sv1.V.value sv2.V.value
- | E.Le -> Z.leq sv1.V.value sv2.V.value
- | E.Ge -> Z.geq sv1.V.value sv2.V.value
- | E.Gt -> Z.gt sv1.V.value sv2.V.value
- | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
- | E.BitOr | E.Shl | E.Shr | E.Ne | E.Eq ->
- failwith "Unreachable"
- in
- Ok
- ({ V.value = V.Concrete (Bool b); ty = T.Bool } : V.typed_value)
- | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
- | E.BitOr -> (
- (* The two operands must have the same type and the result is an integer *)
- assert (sv1.int_ty = sv2.int_ty);
- let res =
- match binop with
- | E.Div ->
- if sv2.V.value = Z.zero then Error ()
- else mk_scalar sv1.int_ty (Z.div sv1.V.value sv2.V.value)
- | E.Rem ->
- (* See [https://github.com/ocaml/Zarith/blob/master/z.mli] *)
- if sv2.V.value = Z.zero then Error ()
- else mk_scalar sv1.int_ty (Z.rem sv1.V.value sv2.V.value)
- | E.Add -> mk_scalar sv1.int_ty (Z.add sv1.V.value sv2.V.value)
- | E.Sub -> mk_scalar sv1.int_ty (Z.sub sv1.V.value sv2.V.value)
- | E.Mul -> mk_scalar sv1.int_ty (Z.mul sv1.V.value sv2.V.value)
- | E.BitXor -> raise Unimplemented
- | E.BitAnd -> raise Unimplemented
- | E.BitOr -> raise Unimplemented
- | E.Lt | E.Le | E.Ge | E.Gt | E.Shl | E.Shr | E.Ne | E.Eq ->
- failwith "Unreachable"
- in
- match res with
- | Error err -> Error err
- | Ok sv ->
- Ok
- {
- V.value = V.Concrete (V.Scalar sv);
- ty = Integer sv1.int_ty;
- })
- | E.Shl | E.Shr -> raise Unimplemented
- | E.Ne | E.Eq -> failwith "Unreachable"
- in
- match res with Error _ -> Error Panic | Ok v -> Ok (ctx, v))
+ (* There are binops which require the two operands to have the same
+ type, and binops for which it is not the case.
+ There are also binops which return booleans, and binops which
+ return integers.
+ *)
+ match binop with
+ | E.Lt | E.Le | E.Ge | E.Gt ->
+ (* The two operands must have the same type and the result is a boolean *)
+ assert (sv1.int_ty = sv2.int_ty);
+ let b =
+ match binop with
+ | E.Lt -> Z.lt sv1.V.value sv2.V.value
+ | E.Le -> Z.leq sv1.V.value sv2.V.value
+ | E.Ge -> Z.geq sv1.V.value sv2.V.value
+ | E.Gt -> Z.gt sv1.V.value sv2.V.value
+ | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
+ | E.BitOr | E.Shl | E.Shr | E.Ne | E.Eq ->
+ failwith "Unreachable"
+ in
+ Ok ({ V.value = V.Concrete (Bool b); ty = T.Bool } : V.typed_value)
+ | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd | E.BitOr
+ -> (
+ (* The two operands must have the same type and the result is an integer *)
+ assert (sv1.int_ty = sv2.int_ty);
+ let res =
+ match binop with
+ | E.Div ->
+ if sv2.V.value = Z.zero then Error ()
+ else mk_scalar sv1.int_ty (Z.div sv1.V.value sv2.V.value)
+ | E.Rem ->
+ (* See [https://github.com/ocaml/Zarith/blob/master/z.mli] *)
+ if sv2.V.value = Z.zero then Error ()
+ else mk_scalar sv1.int_ty (Z.rem sv1.V.value sv2.V.value)
+ | E.Add -> mk_scalar sv1.int_ty (Z.add sv1.V.value sv2.V.value)
+ | E.Sub -> mk_scalar sv1.int_ty (Z.sub sv1.V.value sv2.V.value)
+ | E.Mul -> mk_scalar sv1.int_ty (Z.mul sv1.V.value sv2.V.value)
+ | E.BitXor -> raise Unimplemented
+ | E.BitAnd -> raise Unimplemented
+ | E.BitOr -> raise Unimplemented
+ | E.Lt | E.Le | E.Ge | E.Gt | E.Shl | E.Shr | E.Ne | E.Eq ->
+ failwith "Unreachable"
+ in
+ match res with
+ | Error _ -> Error EPanic
+ | Ok sv ->
+ Ok
+ {
+ V.value = V.Concrete (V.Scalar sv);
+ ty = Integer sv1.int_ty;
+ })
+ | E.Shl | E.Shr -> raise Unimplemented
+ | E.Ne | E.Eq -> failwith "Unreachable")
| _ -> failwith "Invalid inputs for binop"
-let eval_binary_op_symbolic (config : C.config) (binop : E.binop)
- (op1 : E.operand) (op2 : E.operand) :
- (C.eval_ctx * V.typed_value) eval_result =
+let eval_binary_op_concrete (config : C.config) (binop : E.binop)
+ (op1 : E.operand) (op2 : E.operand)
+ (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
(* Evaluate the operands *)
- let ctx, v1, v2 = eval_two_operands config ctx op1 op2 in
- (* Generate a fresh symbolic value to store the result *)
- let res_sv_id = C.fresh_symbolic_value_id () in
- let res_sv_ty =
- if binop = Eq || binop = Ne then (
- (* Equality operations *)
- assert (v1.ty = v2.ty);
- (* Equality/inequality check is primitive only for a subset of types *)
- assert (ty_is_primitively_copyable v1.ty);
- T.Bool)
- else
- (* Other operations: input types are integers *)
- match (v1.V.ty, v2.V.ty) with
- | T.Integer int_ty1, T.Integer int_ty2 -> (
- match binop with
- | E.Lt | E.Le | E.Ge | E.Gt ->
- assert (int_ty1 = int_ty2);
- T.Bool
- | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
- | E.BitOr ->
- assert (int_ty1 = int_ty2);
- T.Integer int_ty1
- | E.Shl | E.Shr -> raise Unimplemented
- | E.Ne | E.Eq -> failwith "Unreachable")
- | _ -> failwith "Invalid inputs for binop"
+ let eval_ops = eval_two_operands config op1 op2 in
+ (* Compute the result of the binop *)
+ let compute cf (res : V.typed_value * V.typed_value) =
+ let v1, v2 = res in
+ cf (eval_binary_op_concrete_compute config binop v1 v2)
in
- let res_sv =
- { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty }
+ (* Compose and apply *)
+ comp eval_ops compute cf
+
+let eval_binary_op_symbolic (config : C.config) (binop : E.binop)
+ (op1 : E.operand) (op2 : E.operand)
+ (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
+ (* Evaluate the operands *)
+ let eval_ops = eval_two_operands config op1 op2 in
+ (* Compute the result of applying the binop *)
+ let compute cf ((v1, v2) : V.typed_value * V.typed_value) : m_fun =
+ (* Generate a fresh symbolic value to store the result *)
+ let res_sv_id = C.fresh_symbolic_value_id () in
+ let res_sv_ty =
+ if binop = Eq || binop = Ne then (
+ (* Equality operations *)
+ assert (v1.ty = v2.ty);
+ (* Equality/inequality check is primitive only for a subset of types *)
+ assert (ty_is_primitively_copyable v1.ty);
+ T.Bool)
+ else
+ (* Other operations: input types are integers *)
+ match (v1.V.ty, v2.V.ty) with
+ | T.Integer int_ty1, T.Integer int_ty2 -> (
+ match binop with
+ | E.Lt | E.Le | E.Ge | E.Gt ->
+ assert (int_ty1 = int_ty2);
+ T.Bool
+ | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
+ | E.BitOr ->
+ assert (int_ty1 = int_ty2);
+ T.Integer int_ty1
+ | E.Shl | E.Shr -> raise Unimplemented
+ | E.Ne | E.Eq -> failwith "Unreachable")
+ | _ -> failwith "Invalid inputs for binop"
+ in
+ let res_sv =
+ { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty }
+ in
+ (* Synthesize *)
+ S.synthesize_binary_op binop v1 v2 res_sv;
+ (* Call the continuattion *)
+ let v = mk_typed_value_from_symbolic_value res_sv in
+ cf (Ok v)
in
- (* Synthesize *)
- S.synthesize_binary_op binop v1 v2 res_sv;
- (* Return *)
- Ok (ctx, mk_typed_value_from_symbolic_value res_sv)
+ (* Compose and apply *)
+ comp eval_ops compute cf
let eval_binary_op (config : C.config) (binop : E.binop) (op1 : E.operand)
- (op2 : E.operand) : (C.eval_ctx * V.typed_value) eval_result =
+ (op2 : E.operand) (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun
+ =
match config.mode with
- | C.ConcreteMode -> eval_binary_op_concrete config ctx binop op1 op2
- | C.SymbolicMode -> eval_binary_op_symbolic config ctx binop op1 op2
+ | C.ConcreteMode -> eval_binary_op_concrete config binop op1 op2 cf
+ | C.SymbolicMode -> eval_binary_op_symbolic config binop op1 op2 cf
(** Evaluate the discriminant of a concrete (i.e., non symbolic) ADT value *)
let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place)