diff options
| -rw-r--r-- | src/InterpreterExpressions.ml | 35 | ||||
| -rw-r--r-- | src/ValuesUtils.ml | 10 | ||||
| -rw-r--r-- | tests/misc/NoNestedBorrows.fst | 14 |
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 + |