diff --git a/lib/pulse/lib/Pulse.Lib.Mutex.fst b/lib/pulse/lib/Pulse.Lib.Mutex.fst index 3ee693b8a..4e441a027 100644 --- a/lib/pulse/lib/Pulse.Lib.Mutex.fst +++ b/lib/pulse/lib/Pulse.Lib.Mutex.fst @@ -20,6 +20,7 @@ open Pulse.Lib.Core open Pulse.Lib.Reference open Pulse.Lib.SpinLock +module R = Pulse.Lib.Reference module B = Pulse.Lib.Box open Pulse.Main @@ -30,12 +31,20 @@ type mutex (a:Type0) : Type0 = { l:lock; } +let mutex_guard a = R.ref a + let lock_inv (#a:Type0) (r:B.box a) (v:a -> vprop) : (w:vprop { (forall x. is_big (v x)) ==> is_big w }) = exists* x. B.pts_to r x ** v x let mutex_live #a m #p v = lock_alive m.l #p (lock_inv m.r v) +let pts_to mg #p x = R.pts_to mg #p x + +let op_Bang #a mg #x #p = R.op_Bang #a mg #x #p +let op_Colon_Equals #a r y #x = R.op_Colon_Equals #a r y #x +let replace #a r y #x = R.replace #a r y #x + ```pulse fn new_mutex' (#a:Type0) (v:a -> vprop { forall x. is_big (v x) }) (x:a) requires v x @@ -55,21 +64,23 @@ fn new_mutex' (#a:Type0) (v:a -> vprop { forall x. is_big (v x) }) (x:a) let new_mutex = new_mutex' -let belongs_to_mutex (#a:Type0) (r:ref a) (m:mutex a) : vprop = +let belongs_to (#a:Type0) (r:mutex_guard a) (m:mutex a) : vprop = pure (r == B.box_to_ref m.r) ** lock_acquired m.l ```pulse fn lock' (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a) requires mutex_live m #p v - returns r:ref a - ensures mutex_live m #p v ** r `belongs_to_mutex` m ** (exists* x. pts_to r x ** v x) + returns r:mutex_guard a + ensures mutex_live m #p v ** r `belongs_to` m ** (exists* x. pts_to r x ** v x) { unfold (mutex_live m#p v); acquire m.l; unfold lock_inv; - fold (belongs_to_mutex (B.box_to_ref m.r) m); + fold (belongs_to (B.box_to_ref m.r) m); fold (mutex_live m #p v); B.to_ref_pts_to m.r; + with _x. rewrite (R.pts_to (B.box_to_ref m.r) _x) as + (pts_to (B.box_to_ref m.r) _x); B.box_to_ref m.r } ``` @@ -77,13 +88,13 @@ fn lock' (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a) let lock = lock' ```pulse -fn unlock' (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a) (r:ref a) - requires mutex_live m #p v ** r `belongs_to_mutex` m ** (exists* x. pts_to r x ** v x) +fn unlock' (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a) (mg:mutex_guard a) + requires mutex_live m #p v ** mg `belongs_to` m ** (exists* x. pts_to mg x ** v x) ensures mutex_live m #p v { unfold (mutex_live m #p v); - unfold (r `belongs_to_mutex` m); - with x. rewrite (pts_to r x) as (pts_to (B.box_to_ref m.r) x); + unfold (mg `belongs_to` m); + with x. rewrite (pts_to mg x) as (R.pts_to (B.box_to_ref m.r) x); B.to_box_pts_to m.r; fold lock_inv; release m.l; diff --git a/lib/pulse/lib/Pulse.Lib.Mutex.fsti b/lib/pulse/lib/Pulse.Lib.Mutex.fsti index 5b049ce2f..5436c49a9 100644 --- a/lib/pulse/lib/Pulse.Lib.Mutex.fsti +++ b/lib/pulse/lib/Pulse.Lib.Mutex.fsti @@ -24,36 +24,53 @@ module T = FStar.Tactics.V2 // A model of Rust mutex // -// -// Can we make the specs more precise? E.g., log the values in an append-only log -// and say that at the time of locking the box value appears later than any (stable) snapshot -// of the log? -// - val mutex (a:Type0) : Type0 +val mutex_guard (a:Type0) : Type0 + val mutex_live (#a:Type0) (m:mutex a) (#[T.exact (`1.0R)] p:perm) (v:a -> vprop) : vprop +// +// mutex_guard is a ref-like type +// + +val pts_to (#a:Type0) (mg:mutex_guard a) (#[T.exact (`1.0R)] p:perm) (x:a) : vprop + +val ( ! ) (#a:Type0) (mg:mutex_guard a) (#x:erased a) (#p:perm) + : stt a + (requires pts_to mg #p x) + (ensures fun y -> pts_to mg #p x ** pure (reveal x == y)) + +val ( := ) (#a:Type0) (mg:mutex_guard a) (y:a) (#x:erased a) + : stt unit + (requires mg `pts_to` x) + (ensures fun _ -> mg `pts_to` y) + +val replace (#a:Type0) (mg:mutex_guard a) (y:a) (#x:erased a) + : stt a + (requires mg `pts_to` x) + (ensures fun r -> mg `pts_to` y ** pure (r == reveal x)) + val new_mutex (#a:Type0) (v:a -> vprop { forall x. is_big (v x) }) (x:a) : stt (mutex a) - (requires v x) - (ensures fun m -> mutex_live m v) + (requires v x) + (ensures fun m -> mutex_live m v) -val belongs_to_mutex (#a:Type0) (r:ref a) (m:mutex a) : vprop +val belongs_to (#a:Type0) (mg:mutex_guard a) (m:mutex a) : vprop val lock (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a) - : stt (ref a) - (requires mutex_live m #p v) - (ensures fun r -> mutex_live m #p v ** r `belongs_to_mutex` m ** (exists* x. pts_to r x ** v x)) + : stt (mutex_guard a) + (requires mutex_live m #p v) + (ensures fun mg -> mutex_live m #p v ** mg `belongs_to` m ** (exists* x. pts_to mg x ** v x)) -val unlock (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a) (r:ref a) +val unlock (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a) (mg:mutex_guard a) : stt unit - (requires mutex_live m #p v ** r `belongs_to_mutex` m ** (exists* x. pts_to r x ** v x)) - (ensures fun _ -> mutex_live m #p v) + (requires mutex_live m #p v ** mg `belongs_to` m ** (exists* x. pts_to mg x ** v x)) + (ensures fun _ -> mutex_live m #p v) val share (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a) : stt_ghost unit emp_inames diff --git a/pulse2rust/src/Pulse2Rust.Extract.fst b/pulse2rust/src/Pulse2Rust.Extract.fst index c57691a38..a62466f6b 100644 --- a/pulse2rust/src/Pulse2Rust.Extract.fst +++ b/pulse2rust/src/Pulse2Rust.Extract.fst @@ -91,8 +91,6 @@ let type_of (g:env) (e:expr) : bool = // is_mut | _ -> false - // | _ -> fail_nyi (format1 "type_of %s" (expr_to_string e)) - // // rust functions are uncurried // @@ -418,7 +416,8 @@ let rec lb_init_and_def (g:env) (lb:S.mllb) match lb.mllb_def.expr with | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, _) -> S.string_of_mlpath p = "Pulse.Lib.Vec.alloc" || - S.string_of_mlpath p = "Pulse.Lib.Box.alloc" + S.string_of_mlpath p = "Pulse.Lib.Box.alloc" || + S.string_of_mlpath p = "Pulse.Lib.Mutex.lock" | _ -> false in is_mut, lb.mllb_tysc |> must |> snd |> extract_mlty g, @@ -473,20 +472,25 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr = | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, [e1; e2; _]) when S.string_of_mlpath p = "Pulse.Lib.Reference.op_Colon_Equals" || - S.string_of_mlpath p = "Pulse.Lib.Box.op_Colon_Equals" -> + S.string_of_mlpath p = "Pulse.Lib.Box.op_Colon_Equals" || + S.string_of_mlpath p = "Pulse.Lib.Mutex.op_Colon_Equals" -> let e1 = extract_mlexpr g e1 in let e2 = extract_mlexpr g e2 in let b = type_of g e1 in - if b - then mk_assign e1 e2 - else mk_ref_assign e1 e2 + let is_mutex_guard = S.string_of_mlpath p = "Pulse.Lib.Mutex.op_Colon_Equals" in + if is_mutex_guard || not b + then mk_ref_assign e1 e2 + else mk_assign e1 e2 | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, [e; _; _]) when S.string_of_mlpath p = "Pulse.Lib.Reference.op_Bang" || - S.string_of_mlpath p = "Pulse.Lib.Box.op_Bang" -> + S.string_of_mlpath p = "Pulse.Lib.Box.op_Bang" || + S.string_of_mlpath p = "Pulse.Lib.Mutex.op_Bang" -> let e = extract_mlexpr g e in let b = type_of g e in - if b then e - else mk_ref_read e + let is_mutex_guard = S.string_of_mlpath p = "Pulse.Lib.Mutex.op_Colon_Equals" in + if is_mutex_guard || not b + then mk_ref_read e + else e | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, _)}, [e1; e2; _]) when S.string_of_mlpath p = "Pulse.Lib.Pervasives.ref_apply" -> @@ -528,7 +532,7 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr = let e3 = extract_mlexpr g e3 in mk_assign (mk_expr_index e1 e2) e3 - | S.MLE_App ({ expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e_v::e_i::e_x::_) + | S.MLE_App ({ expr=S.MLE_TApp ({expr=S.MLE_Name p}, [a])}, e_v::e_i::e_x::_) when S.string_of_mlpath p = "Pulse.Lib.Vec.replace_i" || S.string_of_mlpath p = "Pulse.Lib.Vec.replace_i_ref" -> @@ -536,12 +540,16 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr = let e_i = extract_mlexpr g e_i in let e_x = extract_mlexpr g e_x in let is_mut = true in - mk_mem_replace (mk_reference_expr is_mut (mk_expr_index e_v e_i)) e_x + mk_mem_replace (extract_mlty g a) + (mk_reference_expr is_mut (mk_expr_index e_v e_i)) e_x - | S.MLE_App ({ expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e_r::e_x::_) + | S.MLE_App ({ expr=S.MLE_TApp ({expr=S.MLE_Name p}, [a])}, e_r::e_x::_) when S.string_of_mlpath p = "Pulse.Lib.Reference.replace" -> - - mk_mem_replace (extract_mlexpr g e_r) (extract_mlexpr g e_x) + + mk_mem_replace (extract_mlty g a) + (extract_mlexpr g e_r) + (extract_mlexpr g e_x) + // // vec_as_array e extracted to &mut e @@ -580,6 +588,18 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr = when S.string_of_mlpath p = "Pulse.Lib.Mutex.lock" -> let e = extract_mlexpr g e in mk_lock_mutex e + | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, _::_::_::e::_) + when S.string_of_mlpath p = "Pulse.Lib.Mutex.unlock" -> + let e = extract_mlexpr g e in + mk_unlock_mutex e + | S.MLE_App ({ expr=S.MLE_TApp ({expr=S.MLE_Name p}, [a])}, e_mg::e_x::_) + when S.string_of_mlpath p = "Pulse.Lib.Mutex.replace" -> + + let is_mut = true in + mk_mem_replace (extract_mlty g a) + (mk_reference_expr is_mut (extract_mlexpr g e_mg)) + (extract_mlexpr g e_x) + | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, [e1; e2]) when S.string_of_mlpath p = "Pulse.Lib.Array.Core.free" -> @@ -680,29 +700,18 @@ and extract_mlexpr_to_stmts (g:env) (e:S.mlexpr) : list stmt = | S.MLE_Let ((S.NonRec, [lb]), e) -> begin - match lb.mllb_def.expr with - | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, _)}, _) - when S.mlpath_to_string p = "Pulse.Lib.Mutex.unlock" -> - extract_mlexpr_to_stmts g e - | _ -> - let is_mut, ty, init = lb_init_and_def g lb in - let topt = - match lb.mllb_def.expr with - | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, _::e::_) - when S.string_of_mlpath p = "Pulse.Lib.Mutex.lock" -> - Some ty - | _ -> None in - let s = mk_local_stmt - (match lb.mllb_tysc with - | Some (_, S.MLTY_Erased) -> None - | _ -> Some (varname lb.mllb_name)) - topt - is_mut - init in - s::(extract_mlexpr_to_stmts (push_local g lb.mllb_name ty is_mut) e) + let is_mut, ty, init = lb_init_and_def g lb in + let topt = None in + let s = mk_local_stmt + (match lb.mllb_tysc with + | Some (_, S.MLTY_Erased) -> None + | _ -> Some (varname lb.mllb_name)) + topt + is_mut + init in + s::(extract_mlexpr_to_stmts (push_local g lb.mllb_name ty is_mut) e) end - | S.MLE_App ({ expr=S.MLE_TApp ({ expr=S.MLE_Name p }, _) }, _) when S.string_of_mlpath p = "failwith" -> [Stmt_expr (mk_call (mk_expr_path_singl panic_fn) [])] diff --git a/pulse2rust/src/Pulse2Rust.Rust.Syntax.fst b/pulse2rust/src/Pulse2Rust.Rust.Syntax.fst index 3f71b0a94..b50cad0c8 100644 --- a/pulse2rust/src/Pulse2Rust.Rust.Syntax.fst +++ b/pulse2rust/src/Pulse2Rust.Rust.Syntax.fst @@ -169,9 +169,11 @@ let mk_expr_struct (path:list string) (fields:list (string & expr)) : expr = let mk_expr_tuple (l:list expr) : expr = Expr_tuple l -let mk_mem_replace (e:expr) (new_v:expr) : expr = +let mk_mem_replace (t:typ) (e:expr) (new_v:expr) : expr = mk_call - (mk_expr_path ["std"; "mem"; "replace"]) + (Expr_path [{ path_segment_name = "std"; path_segment_generic_args = [] }; + { path_segment_name = "mem"; path_segment_generic_args = [] }; + { path_segment_name = "replace"; path_segment_generic_args = [t] }]) [e; new_v] let mk_method_call (receiver:expr) (name:string) (args:list expr) : expr = @@ -188,9 +190,14 @@ let mk_new_mutex (e:expr) = let mk_lock_mutex (e:expr) : expr = let e_lock = mk_method_call e "lock" [] in - let e_lock_unwrap = mk_method_call e_lock "unwrap" [] in - let is_mut = true in - mk_reference_expr is_mut e_lock_unwrap + mk_method_call e_lock "unwrap" [] + // let is_mut = true in + // mk_reference_expr is_mut e_lock_unwrap + +let mk_unlock_mutex (e:expr) : expr = + mk_call + (mk_expr_path ["std"; "mem"; "drop"]) + [e] let mk_scalar_fn_arg (name:string) (is_mut:bool) (t:typ) = Fn_arg_pat { diff --git a/pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti b/pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti index 9b6344ef5..6a03813ad 100644 --- a/pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti +++ b/pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti @@ -345,11 +345,12 @@ val mk_expr_field (base:expr) (f:string) : expr val mk_expr_field_unnamed (base:expr) (i:int) : expr val mk_expr_struct (path:list string) (fields:list (string & expr)) : expr val mk_expr_tuple (l:list expr) : expr -val mk_mem_replace (e:expr) (new_v:expr) : expr +val mk_mem_replace (t:typ) (e:expr) (new_v:expr) : expr val mk_method_call (receiver:expr) (name:string) (args:list expr) : expr val mk_new_mutex (e:expr) : expr val mk_lock_mutex (e:expr) : expr +val mk_unlock_mutex (e:expr) : expr val mk_local_stmt (name:option string) (t:option typ) (is_mut:bool) (init:expr) : stmt val mk_scalar_fn_arg (name:string) (is_mut:bool) (t:typ) : fn_arg diff --git a/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml b/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml index ad4c1c0ad..f14300b2f 100644 --- a/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml +++ b/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml @@ -621,10 +621,13 @@ let rec (lb_init_and_def : FStar_Extraction_ML_Syntax.loc = uu___5;_}, uu___6) -> - (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Pulse.Lib.Vec.alloc") || + ((let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.Vec.alloc") || + (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.Box.alloc")) + || (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Pulse.Lib.Box.alloc") + uu___7 = "Pulse.Lib.Mutex.lock") | uu___1 -> false in let uu___1 = let uu___2 = @@ -758,17 +761,23 @@ and (extract_mlexpr : FStar_Extraction_ML_Syntax.loc = uu___4;_}, e1::e2::uu___5::[]) when - (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.Reference.op_Colon_Equals") || + ((let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.Reference.op_Colon_Equals") || + (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.Box.op_Colon_Equals")) + || (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.Box.op_Colon_Equals") + uu___6 = "Pulse.Lib.Mutex.op_Colon_Equals") -> let e11 = extract_mlexpr g e1 in let e21 = extract_mlexpr g e2 in let b = type_of g e11 in - if b - then Pulse2Rust_Rust_Syntax.mk_assign e11 e21 - else Pulse2Rust_Rust_Syntax.mk_ref_assign e11 e21 + let is_mutex_guard = + let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___6 = "Pulse.Lib.Mutex.op_Colon_Equals" in + if is_mutex_guard || (Prims.op_Negation b) + then Pulse2Rust_Rust_Syntax.mk_ref_assign e11 e21 + else Pulse2Rust_Rust_Syntax.mk_assign e11 e21 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -783,14 +792,22 @@ and (extract_mlexpr : FStar_Extraction_ML_Syntax.loc = uu___4;_}, e1::uu___5::uu___6::[]) when - (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Pulse.Lib.Reference.op_Bang") || + ((let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.Reference.op_Bang") || + (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.Box.op_Bang")) + || (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Pulse.Lib.Box.op_Bang") + uu___7 = "Pulse.Lib.Mutex.op_Bang") -> let e2 = extract_mlexpr g e1 in let b = type_of g e2 in - if b then e2 else Pulse2Rust_Rust_Syntax.mk_ref_read e2 + let is_mutex_guard = + let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.Mutex.op_Colon_Equals" in + if is_mutex_guard || (Prims.op_Negation b) + then Pulse2Rust_Rust_Syntax.mk_ref_read e2 + else e2 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -911,24 +928,25 @@ and (extract_mlexpr : FStar_Extraction_ML_Syntax.MLE_Name p; FStar_Extraction_ML_Syntax.mlty = uu___; FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2::[]); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - e_v::e_i::e_x::uu___5) + a::[]); + FStar_Extraction_ML_Syntax.mlty = uu___2; + FStar_Extraction_ML_Syntax.loc = uu___3;_}, + e_v::e_i::e_x::uu___4) when - (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.Vec.replace_i") || - (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.Vec.replace_i_ref") + (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Pulse.Lib.Vec.replace_i") || + (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Pulse.Lib.Vec.replace_i_ref") -> let e_v1 = extract_mlexpr g e_v in let e_i1 = extract_mlexpr g e_i in let e_x1 = extract_mlexpr g e_x in let is_mut = true in + let uu___5 = extract_mlty g a in let uu___6 = let uu___7 = Pulse2Rust_Rust_Syntax.mk_expr_index e_v1 e_i1 in Pulse2Rust_Rust_Syntax.mk_reference_expr is_mut uu___7 in - Pulse2Rust_Rust_Syntax.mk_mem_replace uu___6 e_x1 + Pulse2Rust_Rust_Syntax.mk_mem_replace uu___5 uu___6 e_x1 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -938,16 +956,17 @@ and (extract_mlexpr : FStar_Extraction_ML_Syntax.MLE_Name p; FStar_Extraction_ML_Syntax.mlty = uu___; FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2::[]); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - e_r::e_x::uu___5) + a::[]); + FStar_Extraction_ML_Syntax.mlty = uu___2; + FStar_Extraction_ML_Syntax.loc = uu___3;_}, + e_r::e_x::uu___4) when - let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___6 = "Pulse.Lib.Reference.replace" -> + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Pulse.Lib.Reference.replace" -> + let uu___5 = extract_mlty g a in let uu___6 = extract_mlexpr g e_r in let uu___7 = extract_mlexpr g e_x in - Pulse2Rust_Rust_Syntax.mk_mem_replace uu___6 uu___7 + Pulse2Rust_Rust_Syntax.mk_mem_replace uu___5 uu___6 uu___7 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -1067,6 +1086,47 @@ and (extract_mlexpr : uu___8 = "Pulse.Lib.Mutex.lock" -> let e2 = extract_mlexpr g e1 in Pulse2Rust_Rust_Syntax.mk_lock_mutex e2 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2::[]); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + uu___5::uu___6::uu___7::e1::uu___8) + when + let uu___9 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___9 = "Pulse.Lib.Mutex.unlock" -> + let e2 = extract_mlexpr g e1 in + Pulse2Rust_Rust_Syntax.mk_unlock_mutex e2 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + a::[]); + FStar_Extraction_ML_Syntax.mlty = uu___2; + FStar_Extraction_ML_Syntax.loc = uu___3;_}, + e_mg::e_x::uu___4) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Pulse.Lib.Mutex.replace" -> + let is_mut = true in + let uu___5 = extract_mlty g a in + let uu___6 = + let uu___7 = extract_mlexpr g e_mg in + Pulse2Rust_Rust_Syntax.mk_reference_expr is_mut uu___7 in + let uu___7 = extract_mlexpr g e_x in + Pulse2Rust_Rust_Syntax.mk_mem_replace uu___5 uu___6 uu___7 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -1356,69 +1416,27 @@ and (extract_mlexpr_to_stmts : -> extract_mlexpr_to_stmts g e1 | FStar_Extraction_ML_Syntax.MLE_Let ((FStar_Extraction_ML_Syntax.NonRec, lb::[]), e1) -> - (match (lb.FStar_Extraction_ML_Syntax.mllb_def).FStar_Extraction_ML_Syntax.expr - with - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - uu___5) - when - (FStar_Extraction_ML_Syntax.mlpath_to_string p) = - "Pulse.Lib.Mutex.unlock" - -> extract_mlexpr_to_stmts g e1 - | uu___ -> - let uu___1 = lb_init_and_def g lb in - (match uu___1 with - | (is_mut, ty, init) -> - let topt = - match (lb.FStar_Extraction_ML_Syntax.mllb_def).FStar_Extraction_ML_Syntax.expr - with - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___2; - FStar_Extraction_ML_Syntax.loc = uu___3;_}, - uu___4::[]); - FStar_Extraction_ML_Syntax.mlty = uu___5; - FStar_Extraction_ML_Syntax.loc = uu___6;_}, - uu___7::e2::uu___8) - when - let uu___9 = - FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___9 = "Pulse.Lib.Mutex.lock" -> - FStar_Pervasives_Native.Some ty - | uu___2 -> FStar_Pervasives_Native.None in - let s = - let uu___2 = - match lb.FStar_Extraction_ML_Syntax.mllb_tysc with - | FStar_Pervasives_Native.Some - (uu___3, FStar_Extraction_ML_Syntax.MLTY_Erased) - -> FStar_Pervasives_Native.None - | uu___3 -> - let uu___4 = - varname lb.FStar_Extraction_ML_Syntax.mllb_name in - FStar_Pervasives_Native.Some uu___4 in - Pulse2Rust_Rust_Syntax.mk_local_stmt uu___2 topt is_mut - init in - let uu___2 = - let uu___3 = - Pulse2Rust_Env.push_local g - lb.FStar_Extraction_ML_Syntax.mllb_name ty is_mut in - extract_mlexpr_to_stmts uu___3 e1 in - s :: uu___2)) + let uu___ = lb_init_and_def g lb in + (match uu___ with + | (is_mut, ty, init) -> + let topt = FStar_Pervasives_Native.None in + let s = + let uu___1 = + match lb.FStar_Extraction_ML_Syntax.mllb_tysc with + | FStar_Pervasives_Native.Some + (uu___2, FStar_Extraction_ML_Syntax.MLTY_Erased) -> + FStar_Pervasives_Native.None + | uu___2 -> + let uu___3 = + varname lb.FStar_Extraction_ML_Syntax.mllb_name in + FStar_Pervasives_Native.Some uu___3 in + Pulse2Rust_Rust_Syntax.mk_local_stmt uu___1 topt is_mut init in + let uu___1 = + let uu___2 = + Pulse2Rust_Env.push_local g + lb.FStar_Extraction_ML_Syntax.mllb_name ty is_mut in + extract_mlexpr_to_stmts uu___2 e1 in + s :: uu___1) | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = diff --git a/pulse2rust/src/ocaml/generated/Pulse2Rust_Rust_Syntax.ml b/pulse2rust/src/ocaml/generated/Pulse2Rust_Rust_Syntax.ml index c796fb1ea..39a4f63a9 100644 --- a/pulse2rust/src/ocaml/generated/Pulse2Rust_Rust_Syntax.ml +++ b/pulse2rust/src/ocaml/generated/Pulse2Rust_Rust_Syntax.ml @@ -1037,11 +1037,16 @@ let (mk_expr_struct : { expr_struct_path = path; expr_struct_fields = uu___1 } in Expr_struct uu___ let (mk_expr_tuple : expr Prims.list -> expr) = fun l -> Expr_tuple l -let (mk_mem_replace : expr -> expr -> expr) = - fun e -> - fun new_v -> - let uu___ = mk_expr_path ["std"; "mem"; "replace"] in - mk_call uu___ [e; new_v] +let (mk_mem_replace : typ -> expr -> expr -> expr) = + fun t -> + fun e -> + fun new_v -> + mk_call + (Expr_path + [{ path_segment_name = "std"; path_segment_generic_args = [] }; + { path_segment_name = "mem"; path_segment_generic_args = [] }; + { path_segment_name = "replace"; path_segment_generic_args = [t] + }]) [e; new_v] let (mk_method_call : expr -> Prims.string -> expr Prims.list -> expr) = fun receiver -> fun name -> @@ -1059,8 +1064,10 @@ let (mk_new_mutex : expr -> expr) = let (mk_lock_mutex : expr -> expr) = fun e -> let e_lock = mk_method_call e "lock" [] in - let e_lock_unwrap = mk_method_call e_lock "unwrap" [] in - let is_mut = true in mk_reference_expr is_mut e_lock_unwrap + mk_method_call e_lock "unwrap" [] +let (mk_unlock_mutex : expr -> expr) = + fun e -> + let uu___ = mk_expr_path ["std"; "mem"; "drop"] in mk_call uu___ [e] let (mk_scalar_fn_arg : Prims.string -> Prims.bool -> typ -> fn_arg) = fun name -> fun is_mut -> diff --git a/pulse2rust/src/ocaml/rust/src/lib.rs b/pulse2rust/src/ocaml/rust/src/lib.rs index 90364d169..c15ceca07 100644 --- a/pulse2rust/src/ocaml/rust/src/lib.rs +++ b/pulse2rust/src/ocaml/rust/src/lib.rs @@ -727,7 +727,24 @@ fn to_syn_path(s: &Vec) -> syn::Path { s.iter().for_each(|s| { segs.push(syn::PathSegment { ident: Ident::new(&s.path_segment_name, Span::call_site()), - arguments: PathArguments::None, + arguments: if s.path_segment_generic_args.len() == 0 { + PathArguments::None + } else { + let mut args: Punctuated = Punctuated::new(); + s.path_segment_generic_args + .iter() + .for_each(|a| args.push(syn::GenericArgument::Type(to_syn_typ(a)))); + PathArguments::AngleBracketed(syn::AngleBracketedGenericArguments { + colon2_token: None, + lt_token: syn::token::Lt { + spans: [Span::call_site()], + }, + args, + gt_token: syn::token::Gt { + spans: [Span::call_site()], + }, + }) + }, }) }); Path { @@ -2328,3 +2345,13 @@ ocaml_export! { // z.to_string().to_owned().to_ocaml(cr) // } } + +// use std::sync::Mutex; + +// fn test(m: Mutex) -> Mutex(&mut data, 6); +// let y = *data; +// drop(data); +// } diff --git a/pulse2rust/tests/src/dpe_/dpe.rs b/pulse2rust/tests/src/dpe_/dpe.rs index c2771b678..f4f3492c0 100644 --- a/pulse2rust/tests/src/dpe_/dpe.rs +++ b/pulse2rust/tests/src/dpe_/dpe.rs @@ -205,20 +205,22 @@ pub fn open_session_aux( } } pub fn open_session(uu___: ()) -> std::option::Option { - let r: &mut std::option::Option = &mut super::dpe::global_state - .lock() - .unwrap(); - let st_opt = std::mem::replace(r, None); + let mut r = super::dpe::global_state.lock().unwrap(); + let st_opt = std::mem::replace::< + std::option::Option, + >(&mut r, None); match st_opt { None => { let st = super::dpe::mk_global_state(()); let res = super::dpe::open_session_aux(st); *r = Some(res.0); + std::mem::drop(r); res.1 } Some(mut st) => { let res = super::dpe::open_session_aux(st); *r = Some(res.0); + std::mem::drop(r); res.1 } } @@ -250,12 +252,15 @@ pub fn take_session_state( sid: super::dpe::sid_t, replace_with: super::dpe::session_state, ) -> std::option::Option { - let r: &mut std::option::Option = &mut super::dpe::global_state - .lock() - .unwrap(); - let st_opt = std::mem::replace(r, None); + let mut r = super::dpe::global_state.lock().unwrap(); + let st_opt = std::mem::replace::< + std::option::Option, + >(&mut r, None); match st_opt { - None => None, + None => { + std::mem::drop(r); + None + } Some(mut st) => { let ctr = st.session_id_counter; let tbl = st.session_table; @@ -277,6 +282,7 @@ pub fn take_session_state( session_table: ok.0, }; *r = Some(st1); + std::mem::drop(r); Some(ok.1) } None => { @@ -285,6 +291,7 @@ pub fn take_session_state( session_table: ss.0, }; *r = Some(st1); + std::mem::drop(r); None } } @@ -294,6 +301,7 @@ pub fn take_session_state( session_table: ss.0, }; *r = Some(st1); + std::mem::drop(r); None } } else { @@ -302,6 +310,7 @@ pub fn take_session_state( session_table: tbl, }; *r = Some(st1); + std::mem::drop(r); None } } diff --git a/pulse2rust/tests/src/dpe_/pulse_lib_hashtable.rs b/pulse2rust/tests/src/dpe_/pulse_lib_hashtable.rs index e619ea1bc..4f084b46a 100644 --- a/pulse2rust/tests/src/dpe_/pulse_lib_hashtable.rs +++ b/pulse2rust/tests/src/dpe_/pulse_lib_hashtable.rs @@ -53,10 +53,9 @@ pub fn replace( ) -> (super::pulse_lib_hashtable_type::ht_t, VT) { let hashf = ht.hashf; let mut contents = ht.contents; - let v_ = std::mem::replace( - &mut contents[idx], - super::pulse_lib_hashtable::mk_used_cell(k, v), - ); + let v_ = std::mem::replace::< + super::pulse_lib_hashtable_spec::cell, + >(&mut contents[idx], super::pulse_lib_hashtable::mk_used_cell(k, v)); let vcontents = contents; let ht1 = super::pulse_lib_hashtable::mk_ht(ht.sz, hashf, vcontents); let _bind_c = match v_ { @@ -96,22 +95,25 @@ pub fn lookup( match opt_sum { Some(mut sum) => { let idx = super::pulse_lib_hashtable::size_t_mod(sum, ht.sz); - let c = std::mem::replace( - &mut contents[idx], - super::pulse_lib_hashtable_spec::cell::Zombie, - ); + let c = std::mem::replace::< + super::pulse_lib_hashtable_spec::cell, + >(&mut contents[idx], super::pulse_lib_hashtable_spec::cell::Zombie); match c { super::pulse_lib_hashtable_spec::cell::Used(mut k_, mut v_) => { if k_ == k { cont = false; ret = Some(idx); - let uu___2 = std::mem::replace( + let uu___2 = std::mem::replace::< + super::pulse_lib_hashtable_spec::cell, + >( &mut contents[idx], super::pulse_lib_hashtable_spec::cell::Used(k_, v_), ); } else { off = voff + 1; - let uu___1 = std::mem::replace( + let uu___1 = std::mem::replace::< + super::pulse_lib_hashtable_spec::cell, + >( &mut contents[idx], super::pulse_lib_hashtable_spec::cell::Used(k_, v_), ); @@ -119,11 +121,15 @@ pub fn lookup( } super::pulse_lib_hashtable_spec::cell::Clean => { cont = false; - let uu___1 = std::mem::replace(&mut contents[idx], c); + let uu___1 = std::mem::replace::< + super::pulse_lib_hashtable_spec::cell, + >(&mut contents[idx], c); } super::pulse_lib_hashtable_spec::cell::Zombie => { off = voff + 1; - let uu___1 = std::mem::replace(&mut contents[idx], c); + let uu___1 = std::mem::replace::< + super::pulse_lib_hashtable_spec::cell, + >(&mut contents[idx], c); } } } @@ -175,7 +181,9 @@ pub fn insert( match opt_sum { Some(mut sum) => { let vidx = super::pulse_lib_hashtable::size_t_mod(sum, ht.sz); - let c = std::mem::replace( + let c = std::mem::replace::< + super::pulse_lib_hashtable_spec::cell, + >( &mut contents[vidx], super::pulse_lib_hashtable_spec::cell::Zombie, ); @@ -273,12 +281,13 @@ pub fn not_full( while { let vi = i; if vi < ht.sz { - let c = std::mem::replace( - &mut contents[vi], - super::pulse_lib_hashtable_spec::cell::Zombie, - ); + let c = std::mem::replace::< + super::pulse_lib_hashtable_spec::cell, + >(&mut contents[vi], super::pulse_lib_hashtable_spec::cell::Zombie); let b = super::pulse_lib_hashtable::is_used(c); - let uu___ = std::mem::replace(&mut contents[vi], b.1); + let uu___ = std::mem::replace::< + super::pulse_lib_hashtable_spec::cell, + >(&mut contents[vi], b.1); b.0 } else { false diff --git a/share/pulse/examples/dice/dpe/DPE.fst b/share/pulse/examples/dice/dpe/DPE.fst index b8938f5c8..0194c2998 100644 --- a/share/pulse/examples/dice/dpe/DPE.fst +++ b/share/pulse/examples/dice/dpe/DPE.fst @@ -24,7 +24,7 @@ open EngineCore open L0Types open L0Core -module L = Pulse.Lib.SpinLock +module M = Pulse.Lib.Mutex module A = Pulse.Lib.Array module R = Pulse.Lib.Reference module SZ = FStar.SizeT @@ -443,7 +443,7 @@ fn open_session () ensures mutex_live global_state global_state_mutex_pred { let r = lock global_state; - let st_opt = R.replace r None; + let st_opt = M.replace r None; match st_opt { None -> { @@ -554,7 +554,7 @@ fn take_session_state (sid:sid_t) (replace_with:session_state) session_state_perm (dflt r replace_with) { let r = lock global_state; - let st_opt = R.replace r None; + let st_opt = M.replace r None; match st_opt { None -> {