summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/InterpreterExpressions.ml35
-rw-r--r--src/ValuesUtils.ml10
-rw-r--r--tests/misc/NoNestedBorrows.fst14
3 files changed, 46 insertions, 13 deletions
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 3043bc7a..bd89649b 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -274,7 +274,7 @@ let eval_unary_op_concrete (config : C.config) (unop : E.unop) (op : E.operand)
match mk_scalar sv.int_ty i with
| Error _ -> cf (Error EPanic)
| Ok sv -> cf (Ok { v with V.value = V.Concrete (V.Scalar sv) }))
- | _ -> failwith "Invalid input for unop"
+ | _ -> raise (Failure "Invalid input for unop")
in
comp eval_op apply cf
@@ -291,7 +291,7 @@ let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand)
match (unop, v.V.ty) with
| E.Not, T.Bool -> T.Bool
| E.Neg, T.Integer int_ty -> T.Integer int_ty
- | _ -> failwith "Invalid input for unop"
+ | _ -> raise (Failure "Invalid input for unop")
in
let res_sv =
{ V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty }
@@ -347,7 +347,7 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_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"
+ raise (Failure "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
@@ -370,7 +370,7 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value)
| 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"
+ raise (Failure "Unreachable")
in
match res with
| Error _ -> Error EPanic
@@ -381,8 +381,8 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value)
ty = Integer sv1.int_ty;
})
| E.Shl | E.Shr -> raise Unimplemented
- | E.Ne | E.Eq -> failwith "Unreachable")
- | _ -> failwith "Invalid inputs for binop"
+ | E.Ne | E.Eq -> raise (Failure "Unreachable"))
+ | _ -> raise (Failure "Invalid inputs for binop")
let eval_binary_op_concrete (config : C.config) (binop : E.binop)
(op1 : E.operand) (op2 : E.operand)
@@ -428,8 +428,8 @@ let eval_binary_op_symbolic (config : C.config) (binop : E.binop)
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"
+ | E.Ne | E.Eq -> raise (Failure "Unreachable"))
+ | _ -> raise (Failure "Invalid inputs for binop")
in
let res_sv =
{ V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty }
@@ -462,20 +462,25 @@ let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place)
let prepare = prepare_rplace config expand_prim_copy access p in
(* Read the value *)
let read (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun =
+ (* The value may be shared: we need to ignore the shared loans *)
+ let v = value_strip_shared_loans v in
match v.V.value with
| Adt av -> (
match av.variant_id with
| None ->
- failwith
- "Invalid input for `discriminant`: structure instead of enum"
+ raise
+ (Failure
+ "Invalid input for `discriminant`: structure instead of enum")
| Some variant_id -> (
let id = Z.of_int (T.VariantId.to_int variant_id) in
match mk_scalar Isize id with
- | Error _ -> failwith "Disciminant id out of range"
+ | Error _ -> raise (Failure "Disciminant id out of range")
(* Should really never happen *)
| Ok sv ->
cf { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize }))
- | _ -> failwith "Invalid input for `discriminant`"
+ | _ ->
+ raise
+ (Failure ("Invalid input for `discriminant`: " ^ V.show_typed_value v))
in
(* Compose and apply *)
comp prepare read cf
@@ -496,6 +501,8 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place)
(* Read the value *)
let read (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun =
fun ctx ->
+ (* The value may be shared: we need to ignore the shared loans *)
+ let v = value_strip_shared_loans v in
match v.V.value with
| Adt _ -> eval_rvalue_discriminant_concrete config p cf ctx
| Symbolic sv ->
@@ -507,7 +514,9 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place)
in
(* This time the value is concrete: reevaluate *)
comp cc (eval_rvalue_discriminant_concrete config p) cf ctx
- | _ -> failwith "Invalid input for `discriminant`"
+ | _ ->
+ raise
+ (Failure ("Invalid input for `discriminant`: " ^ V.show_typed_value v))
in
(* Compose and apply *)
comp prepare read cf ctx
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml
index 9aeb15f4..2814615c 100644
--- a/src/ValuesUtils.ml
+++ b/src/ValuesUtils.ml
@@ -115,3 +115,13 @@ let find_first_primitively_copyable_sv_with_borrows (type_infos : TA.type_infos)
obj#visit_typed_value () v;
None
with FoundSymbolicValue sv -> Some sv
+
+(** Strip the outer shared loans in a value.
+ Ex.:
+ `shared_loan {l0, l1} (3 : u32, shared_loan {l2} (4 : u32))` ~~>
+ `(3 : u32, shared_loan {l2} (4 : u32))`
+ *)
+let rec value_strip_shared_loans (v : typed_value) : typed_value =
+ match v.value with
+ | Loan (SharedLoan (_, v')) -> value_strip_shared_loans v'
+ | _ -> v
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index 48186932..d272bb86 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -538,3 +538,17 @@ let _ = assert_norm (test_weird_borrows1_fwd = Return ())
let test_mem_replace_fwd_back (px : u32) : result u32 =
let i = mem_replace_fwd u32 px 1 in if not (i = 0) then Fail else Return 2
+(** [no_nested_borrows::test_shared_borrow_bool1] *)
+let test_shared_borrow_bool1_fwd (b : bool) : result u32 =
+ if b then Return 0 else Return 1
+
+(** [no_nested_borrows::test_shared_borrow_bool2] *)
+let test_shared_borrow_bool2_fwd : result u32 = Return 0
+
+(** [no_nested_borrows::test_shared_borrow_enum1] *)
+let test_shared_borrow_enum1_fwd (l : list_t u32) : result u32 =
+ begin match l with | ListCons i l0 -> Return 1 | ListNil -> Return 0 end
+
+(** [no_nested_borrows::test_shared_borrow_enum2] *)
+let test_shared_borrow_enum2_fwd : result u32 = Return 0
+