[Rust] share_full takes atomic_mask(MaskTop); verifying atomic.rs (ve…

…rifast#692)

The share_full component of the type interpretation now takes atomic_mask(MaskTop) instead of atomic_mask(Nlft). This enables verifying sync::atomic, and in particular that no mixed-size conflicting atomic accesses occur.

Also:
- The precondition of share_full now additionally asserts ref_origin(l) == l.
- Rust has no subobject provenance.
- Started work on atomic.rs: Verified AtomicBool::from_ptr and AtomicBool::store
- If p is a &UnsafeCell, p.get() calls are translated to ref_origin(p) calls.

bin/rust/aliasing.rsspec

@@ -80,7 +80,7 @@ fn reborrow_ref<T>(x: *T) -> *T;
 //@ ens [f]ref_initialized(x) &*& result == x;
 //@ on_unwind_ens false;
 
-fn reborrow_ref_UnsafeCell(x: *_) -> *_;
+fn create_ref_UnsafeCell(x: *_) -> *_;
 //@ req true;
 //@ ens result == x;
 //@ on_unwind_ens false;

bin/rust/prelude_core.rsspec

@@ -145,6 +145,14 @@ fix ptr_add_(p: pointer, offset: i32, elemTypeid: *_) -> pointer {
 pred points_to_<t>(p: *t; v: option<t>);
 pred points_to<t>(p: *t; v: t) = points_to_::<t>(p, some(v));
 
+lem points_to_bool_to_u8(p: *bool);
+    req *p |-> ?b;
+    ens *(p as *u8) |-> b;
+
+lem points_to_u8_to_bool(p: *u8);
+    req *p |-> ?v &*& v == 0 || v == 1;
+    ens *(p as *bool) |-> v == 1;
+
 lem points_to_limits<T>(p: *T);
     req [?f]points_to(p, ?v);
     ens [f]points_to(p, v) &*& f <= 1 &*& object_pointer_within_limits(p, std::mem::size_of::<T>()) == true;

bin/rust/rust_belt/general.rsspec

@@ -196,8 +196,8 @@ lem share_full_borrow<T>(k: lifetime_t, t: thread_id_t, l: *_);
     ens [_](<T>.share)(k, t, l) &*& [q]lifetime_token(k);
 
 lem share_full_borrow_m<T>(k: lifetime_t, t: thread_id_t, l: *_);
-    req type_interp::<T>() &*& atomic_mask(?mask) &*& mask_le(Nlft, mask) == true &*& full_borrow(k, (<T>.full_borrow_content)(t, l)) &*& [?q]lifetime_token(k);
-    ens type_interp::<T>() &*& atomic_mask(mask) &*& [_](<T>.share)(k, t, l) &*& [q]lifetime_token(k);
+    req type_interp::<T>() &*& atomic_mask(MaskTop) &*& full_borrow(k, (<T>.full_borrow_content)(t, l)) &*& [?q]lifetime_token(k);
+    ens type_interp::<T>() &*& atomic_mask(MaskTop) &*& [_](<T>.share)(k, t, l) &*& [q]lifetime_token(k);
 
 lem init_ref_share<T>(k: lifetime_t, t: thread_id_t, p: *T);
     nonghost_callers_only

bin/rust/std/lib.rsspec

@@ -95,6 +95,53 @@ mod intrinsics {
     //@ ens result == ptr as usize - base as usize;
     //@ on_unwind_ens false;
 
+    // atomic_points_to(p, v) is like points_to(p, v) but additionally, it guarantees that place *p is not accessed
+    // with non-read-only mixed-size accesses since converting from points_to to atomic_points_to is possible only
+    // at top mask, which means the conversion can be thought of as happening in a separate machine step.
+    // Furthermore, it guarantees that p is properly aligned for atomic accesses at type T.
+
+    // Note: these specs are sufficient to prove semantic well-typedness of the sync::atomic API, but are not
+    // sufficient to prove arbitrary functional correctness properties. TODO: Extend these specs to also support the latter.
+
+    /*@
+
+    fix atomic_align_of<T>() -> usize;
+
+    lem_auto atomic_align_of_u8();
+        req true;
+        ens atomic_align_of::<u8>() == 1;
+
+    lem_auto atomic_align_of_usize();
+        req true;
+        ens atomic_align_of::<usize>() == std::mem::size_of::<usize>();
+
+    pred atomic_points_to<T>(p: *T, frac: real, inv_: fix(T, bool););
+
+    lem close_atomic_points_to_m<T>(p: *T, inv_: fix(T, bool));
+        req atomic_mask(MaskTop) &*& [?f](*p |-> ?v) &*& p as usize % atomic_align_of::<T>() == 0 &*& inv_(v) == true;
+        ens atomic_mask(MaskTop) &*& atomic_points_to(p, f, inv_);
+
+    lem open_atomic_points_to<T>(p: *T);
+        req atomic_points_to(p, ?f, ?inv_);
+        ens [f](*p |-> ?v) &*& inv_(v) == true;
+
+    @*/
+
+    unsafe fn atomic_store_relaxed<T>(dst: *mut T, val: T);
+    //@ req [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true;
+    //@ ens [f]atomic_points_to(dst, 1, inv_);
+    //@ on_unwind_ens false;
+
+    unsafe fn atomic_store_release<T>(dst: *mut T, val: T);
+    //@ req [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true;
+    //@ ens [f]atomic_points_to(dst, 1, inv_);
+    //@ on_unwind_ens false;
+
+    unsafe fn atomic_store_seqcst<T>(dst: *mut T, val: T);
+    //@ req [?f]atomic_points_to(dst, 1, ?inv_) &*& inv_(val) == true;
+    //@ ens [f]atomic_points_to(dst, 1, inv_);
+    //@ on_unwind_ens false;
+
 }
 
 mod mem {
@@ -247,7 +294,7 @@ mod alloc {
 
     lem alloc_aligned(ptr: *mut u8);
         req [?f]alloc_block(ptr, ?layout);
-        ens [f]alloc_block(ptr, layout) &*& (ptr as usize) % Layout::align_(layout) == 0;
+        ens [f]alloc_block(ptr, layout) &*& (ptr as usize) % Layout::align_(layout) == 0 &*& ref_origin(ptr) == ptr;
 
     @*/
 
@@ -282,8 +329,8 @@ mod alloc {
         ens *l |-> ?alloc &*& Allocator::<A>(t, alloc, alloc_id);
 
     lem share_Allocator_full_borrow_content_<A>(k: lifetime_t, t: thread_id_t, l: *A, alloc_id: any);
-        req type_interp::<A>() &*& atomic_mask(Nlft) &*& full_borrow(k, Allocator_full_borrow_content_::<A>(t, l, alloc_id)) &*& [?q]lifetime_token(k);
-        ens type_interp::<A>() &*& atomic_mask(Nlft) &*& [_](<A>.share(k, t, l)) &*& [q]lifetime_token(k);
+        req type_interp::<A>() &*& atomic_mask(MaskTop) &*& full_borrow(k, Allocator_full_borrow_content_::<A>(t, l, alloc_id)) &*& [?q]lifetime_token(k);
+        ens type_interp::<A>() &*& atomic_mask(MaskTop) &*& [_](<A>.share(k, t, l)) &*& [q]lifetime_token(k);
 
     pred share_allocator_end_token<A>(l: *A, alloc_id: any);
 
@@ -338,6 +385,7 @@ mod alloc {
         if result == 0 {
             true
         } else {
+            ref_origin(result) == result &*&
             result[..Layout::size_(layout)] |-> _ &*& alloc_block(result, layout) &*&
             result as usize % Layout::align_(layout) == 0 &*&
             object_pointer_within_limits(result, Layout::size_(layout)) == true

docs/rust-reference/src/SUMMARY.md

@@ -10,4 +10,5 @@
     - [Function specifications](func-specs.md)
     - [Function body annotations](func-body-annots.md)
     - [Ghost declarations](ghost-decls.md)
+- [Verifying compliance with Rust's pointer aliasing rules](rusts-aliasing-rules.md)
 - [Verifying non-\`unsafe\` functions](non-unsafe-funcs.md)

docs/rust-reference/src/non-unsafe-funcs.md

@@ -98,8 +98,8 @@ If a crate defines a struct S as well as a custom definition of `<S>.share`, the
 
 ```
 lem S_share_full(k: lifetime_t, t: thread_id_t, l: *S)
-    req atomic_mask(Nlft) &*& [?q]lifetime_token(k) &*& full_borrow(k, S_full_borrow_content(t, l));
-    ens atomic_mask(Nlft) &*& [q]lifetime_token(k) &*& [_]S_share(k, t, l);
+    req atomic_mask(MaskTop) &*& [?q]lifetime_token(k) &*& full_borrow(k, S_full_borrow_content(t, l)) &*& ref_origin(l) == l;
+    ens atomic_mask(MaskTop) &*& [q]lifetime_token(k) &*& [_]S_share(k, t, l);
 
 lem S_share_mono(k: lifetime_t, k1: lifetime_t, t: thread_id_t, l: *S)
     req lifetime_inclusion(k1, k) == true &*& [_]S_share(k, t, l);

docs/rust-reference/src/rusts-aliasing-rules.md

@@ -0,0 +1,42 @@
+# Verifying compliance with Rust's pointer aliasing rules
+
+Breaking [Rust's pointer aliasing
+rules](https://doc.rust-lang.org/reference/behavior-considered-undefined.html#r-undefined.alias)
+or mutating [immutable
+bytes](https://doc.rust-lang.org/reference/behavior-considered-undefined.html#r-undefined.immutable)
+is undefined behavior. VeriFast currently verifies (only) the latter.
+
+In particular, it verifies that the memory pointed to by a shared reference,
+except for the memory inside an `UnsafeCell`, is not mutated while the shared
+reference is active. First of all, shared reference creation is treated like the
+creation of a new pointer value, with the same address but a different
+[provenance](https://doc.rust-lang.org/std/ptr/index.html#provenance) from the
+original pointer. Points-to resources for the original pointer cannot be used
+for accesses through the new shared reference.
+
+VeriFast requires, at creation of a shared reference, that the user transfer a
+fraction greater than 0 and less than 1 of the points-to resources for the
+original place to the new shared reference. These resources are transferred back
+to the original reference when the shared reference is *ended* (and only then);
+from that point on, the shared reference is no longer usable.
+
+Specifically, a shared reference creation expression `&E` is treated like a call
+of function `create_ref` in
+[`aliasing.rsspec`](https://github.com/verifast/verifast/blob/master/bin/rust/aliasing.rsspec),
+which is part of the VeriFast for Rust prelude. This function requires that a
+shared reference value has been *precreated* using lemma `precreate_ref`
+declared in the same file. Furthermore, it requires that the new reference has
+been *initialized*.
+
+Memory inside an `UnsafeCell` is exempted from this process; the points-to
+resources for that memory are never transferred. This means that a shared
+reference to an `UnsafeCell` does not directly provide access to the memory
+behind the `UnsafeCell`. To access the memory, the developer has to call
+`UnsafeCell::get`. VeriFast treats calls of this method like calls of logical
+function `ref_origin` (also declared in `aliasing.rsspec`). Therefore, if a
+struct S has a field f of type `UnsafeCell<T>` inside, it is important for
+`<S>.share(k, t, l)` to (directly or indirectly, e.g. via a nonatomic borrow),
+assert points-to resources for `ref_origin(&(*l).f)`. See, for example,
+[cell.rs](https://github.com/verifast/verifast/blob/master/tests/rust/safe_abstraction/cell.rs)
+and
+[mutex.rs](https://github.com/verifast/verifast/blob/master/tests/rust/safe_abstraction/mutex.rs).

src/rust_frontend/vf_mir_translator/vf_mir_translator.ml

@@ -2223,6 +2223,22 @@ module Make (Args : VF_MIR_TRANSLATOR_ARGS) = struct
                         (`TrFnCallRExpr
                           "Invalid (generic) arg(s) for \
                            std::ptr::mut_ptr::<impl *mut T>::is_null"))
+              | "std::ptr::mut_ptr::<impl *const T>::cast"
+              | "std::ptr::mut_ptr::<impl *mut T>::cast" ->
+                  let [ _; Mir.GenArgType gen_arg_ty_info ], [ arg_cpn ] =
+                    (substs, args_cpn)
+                  in
+                  let* tmp_rvalue_binders, [ arg ] =
+                    translate_operands [ (arg_cpn, fn_loc) ]
+                  in
+                  Ok
+                    ( tmp_rvalue_binders,
+                      FnCallResult
+                        (Ast.CastExpr
+                           ( fn_loc,
+                             PtrTypeExpr
+                               (fn_loc, Mir.basic_type_of gen_arg_ty_info),
+                             arg )) )
               | "std::ptr::const_ptr::<impl *const T>::offset"
               | "std::ptr::mut_ptr::<impl *mut T>::offset" -> (
                   match (substs, args_cpn) with
@@ -2351,7 +2367,6 @@ module Make (Args : VF_MIR_TRANSLATOR_ARGS) = struct
                         ],
                       FnCallResult (mk_unit_expr fn_loc) )
               | "std::cell::UnsafeCell::<T>::new"
-              | "std::cell::UnsafeCell::<T>::get"
               | "std::mem::ManuallyDrop::<T>::new"
               | "std::mem::ManuallyDrop::deref"
               | "std::mem::ManuallyDrop::deref_mut" ->
@@ -2360,6 +2375,17 @@ module Make (Args : VF_MIR_TRANSLATOR_ARGS) = struct
                     translate_operands [ (arg_cpn, fn_loc) ]
                   in
                   Ok (tmp_rvalue_binders, FnCallResult arg)
+              | "std::cell::UnsafeCell::<T>::get" ->
+                  let [ arg_cpn ] = args_cpn in
+                  let* tmp_rvalue_binders, [ arg ] =
+                    translate_operands [ (arg_cpn, fn_loc) ]
+                  in
+                  Ok
+                    ( tmp_rvalue_binders,
+                      FnCallResult
+                        (CallExpr
+                           (fn_loc, "ref_origin", [], [], [ LitPat arg ], Static))
+                    )
               | "core::str::<impl str>::as_ptr"
               | "core::slice::<impl [T]>::as_ptr" ->
                   let [ arg_cpn ] = args_cpn in
@@ -2986,20 +3012,29 @@ module Make (Args : VF_MIR_TRANSLATOR_ARGS) = struct
           else
             let place_ty = decode_ty (place_ty_get ref_data_cpn) in
             let is_implicit = is_implicit_get ref_data_cpn in
+            let place_kind = BodyRd.PlaceKind.get (BodyRd.Place.kind_get place_cpn) in
+            (*
+            Printf.printf "ref creation at %s: place_ty=%s, bor_kind=%s, place_kind=%s, is_implicit=%b\n"
+              (Ast.string_of_loc loc)
+              (string_of_decoded_type place_ty)
+              (match bor_kind with Mut -> "Mut" | Shared -> "Shared")
+              (match place_kind with MutableRef -> "MutableRef" | SharedRef -> "SharedRef" | _ -> "Other")
+              is_implicit;
+            *)
             let fn_name =
               match
                 ( place_ty,
                   bor_kind,
-                  BodyRd.PlaceKind.get (BodyRd.Place.kind_get place_cpn),
+                  place_kind,
                   is_implicit )
               with
               | `Str, Shared, SharedRef, _ -> "reborrow_str_ref"
               | `Str, Shared, _, _ -> "create_str_ref"
               | `Slice _, Mut, _, _ -> "create_slice_ref_mut"
               | `Slice _, Shared, SharedRef, _ -> "reborrow_slice_ref"
               | `Slice _, Shared, _, _ -> "create_slice_ref"
-              | `Adt ("std::cell::UnsafeCell", _, _), Shared, SharedRef, _ ->
-                  "reborrow_ref_UnsafeCell"
+              | `Adt ("std::cell::UnsafeCell", _, _), Shared, _, _ ->
+                  "create_ref_UnsafeCell"
               | _, Mut, MutableRef, true -> "reborrow_ref_mut_implicit"
               | _, Mut, MutableRef, _ -> "reborrow_ref_mut"
               | _, Mut, _, _ -> "create_ref_mut"
@@ -5168,14 +5203,14 @@ module Make (Args : VF_MIR_TRANSLATOR_ARGS) = struct
         let params =
           [ lft_param "k"; thread_id_param "t"; void_ptr_param "l" ]
         in
-        let atomic_mask_token =
+        let atomic_mask_token mask =
           CallExpr
             ( adt_def_loc,
               "atomic_mask",
               (*type arguments*) [],
               (*indices*) [],
               (*arguments*)
-              [ lpat_var "Nlft" ],
+              [ lpat_var mask ],
               Static )
         in
         let fbor_pred =
@@ -5217,9 +5252,22 @@ module Make (Args : VF_MIR_TRANSLATOR_ARGS) = struct
             (List.map
                (fun asn -> (adt_def_loc, asn))
                [
-                 atomic_mask_token;
+                 atomic_mask_token "MaskTop";
                  fbor_pred;
                  lft_token (VarPat (adt_def_loc, "q"));
+                 Operation
+                   ( adt_def_loc,
+                     Eq,
+                     [
+                       CallExpr
+                         ( adt_def_loc,
+                           "ref_origin",
+                           [],
+                           [],
+                           [ LitPat (Var (adt_def_loc, "l")) ],
+                           Static );
+                       Var (adt_def_loc, "l");
+                     ] );
                ])
             None
         in
@@ -5244,7 +5292,7 @@ module Make (Args : VF_MIR_TRANSLATOR_ARGS) = struct
           AstAux.list_to_sep_conj
             (List.map
                (fun asn -> (adt_def_loc, asn))
-               [ atomic_mask_token; share_pred "l"; lft_token (lpat_var "q") ])
+               [ atomic_mask_token "MaskTop"; share_pred "l"; lft_token (lpat_var "q") ])
             None
         in
         let post = add_type_interp_asns adt_def_loc tparams post in
@@ -5300,7 +5348,7 @@ module Make (Args : VF_MIR_TRANSLATOR_ARGS) = struct
             (List.map
                (fun asn -> (adt_def_loc, asn))
                [
-                 atomic_mask_token;
+                 atomic_mask_token "Nlft";
                  ref_init_perm;
                  pre_shr_asn;
                  lft_token (VarPat (adt_def_loc, "q"));
@@ -5351,7 +5399,7 @@ module Make (Args : VF_MIR_TRANSLATOR_ARGS) = struct
             (List.map
                (fun asn -> (adt_def_loc, asn))
                [
-                 atomic_mask_token;
+                 atomic_mask_token "Nlft";
                  lft_token (lpat_var "q");
                  post_shr_asn;
                  ref_initialized_asn;

src/verifast.ml

@@ -708,13 +708,14 @@ module VerifyProgram(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
       in
       cont (chunk::h) env
     | ExprStmt (CallExpr (l, "produce_type_interp", targs, indices, args, Static)) when dialect = Some Rust ->
-      let x =
+      let tp =
         match targs, indices, args with
-          [IdentTypeExpr (_, None, x)], [], [] when List.mem x tparams && tparam_carries_typeid x ->
-          x
+          [tp], [], [] ->
+          tp
         | _ ->
           static_error l "Syntax error: produce_type_interp<T>() expected" None
       in
+      let tp = check_pure_type (pn,ilist) tparams Ghost tp in
       begin
         (* Keep this ghost command from being used in the proof of x's proof obligations! *)
         match leminfo with
@@ -723,7 +724,7 @@ module VerifyProgram(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
           | RealFuncInfo (_, _, _) | RealMethodInfo _ -> ()
       end;
       let type_interp_pred_symb = get_pred_symb "type_interp" in
-      let type_interp_chunk = Chunk ((type_interp_pred_symb, true), [GhostTypeParam x], real_unit, [], None) in
+      let type_interp_chunk = Chunk ((type_interp_pred_symb, true), [tp], real_unit, [], None) in
       cont (type_interp_chunk::h) env
     | ExprStmt (CallExpr (l, "free", [], [], args,Static) as e) ->
       let args = List.map (function LitPat e -> e | _ -> static_error l "No patterns allowed here" None ) args in

src/verifast1.ml

@@ -82,7 +82,7 @@ module VerifyProgram1(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
   let fno_strict_aliasing = Vfbindings.get Vfparam_fno_strict_aliasing vfbindings || dialect = Some Rust
   let assume_left_to_right_evaluation = Vfbindings.get Vfparam_assume_left_to_right_evaluation vfbindings
   let assume_no_provenance = Vfbindings.get Vfparam_assume_no_provenance vfbindings
-  let assume_no_subobject_provenance = Vfbindings.get Vfparam_assume_no_subobject_provenance vfbindings
+  let assume_no_subobject_provenance = Vfbindings.get Vfparam_assume_no_subobject_provenance vfbindings || dialect = Some Rust
   let include_paths = Vfbindings.get Vfparam_include_paths vfbindings
   let option_allow_undeclared_struct_types = Vfbindings.get Vfparam_allow_undeclared_struct_types vfbindings
   let data_model = Vfbindings.get Vfparam_data_model vfbindings
@@ -6185,6 +6185,7 @@ module VerifyProgram1(VerifyProgramArgs: VERIFY_PROGRAM_ARGS) = struct
     ctxt#assume_forall "field_ptr_eq_ptr_add" [fp] [ctxt#type_inductive; ctxt#type_inductive; ctxt#type_int] eq
     end;
 
+    if dialect <> Some Rust then
     begin
     ctxt#begin_formal;
     let p = ctxt#mk_bound 0 ctxt#type_inductive in

tests/rust/nonnull.rs

@@ -26,8 +26,8 @@ lem ptr::NonNull_share_mono<T>(k: lifetime_t, k1: lifetime_t, t: thread_id_t, l:
 }
 
 lem ptr::NonNull_share_full<T>(k: lifetime_t, t: thread_id_t, l: *ptr::NonNull<T>)
-    req atomic_mask(Nlft) &*& full_borrow(k, ptr::NonNull_full_borrow_content(t, l)) &*& [?q]lifetime_token(k);
-    ens atomic_mask(Nlft) &*& [_]ptr::NonNull_share(k, t, l) &*& [q]lifetime_token(k);
+    req atomic_mask(MaskTop) &*& full_borrow(k, ptr::NonNull_full_borrow_content(t, l)) &*& [?q]lifetime_token(k);
+    ens atomic_mask(MaskTop) &*& [_]ptr::NonNull_share(k, t, l) &*& [q]lifetime_token(k);
 {
     produce_lem_ptr_chunk implies(ptr::NonNull_frac_bc(t, l), ptr::NonNull_full_borrow_content(t, l))(){
         open ptr::NonNull_frac_bc::<T>(t, l)();