From c707e5cc874f0e7f52c0df0dc81495f515690f8c Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 10 Oct 2024 15:19:55 -0700 Subject: [PATCH] Slice.subslice --- lib/pulse/lib/Pulse.Lib.ArrayPtr.fst | 33 +++++++++++- lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti | 14 ++++- lib/pulse/lib/Pulse.Lib.Slice.Util.fst | 53 +++++++++++++++++++ lib/pulse/lib/Pulse.Lib.Slice.fst | 23 +++++++- lib/pulse/lib/Pulse.Lib.Slice.fsti | 13 +++++ pulse2rust/src/Pulse2Rust.Extract.fst | 4 ++ pulse2rust/src/Pulse2Rust.Rust.Syntax.fst | 7 +++ pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti | 12 +++++ .../src/ocaml/generated/Pulse2Rust_Extract.ml | 30 +++++++++++ .../ocaml/generated/Pulse2Rust_Rust_Syntax.ml | 47 ++++++++++++++++ pulse2rust/src/ocaml/rust/src/lib.rs | 48 +++++++++++++++++ pulse2rust/tests/src/example_slice.rs | 6 ++- share/pulse/examples/Example.Slice.fst | 9 ++-- src/extraction/ExtractPulse.fst | 2 +- src/ocaml/plugin/generated/ExtractPulse.ml | 2 +- 15 files changed, 294 insertions(+), 9 deletions(-) diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst index 11afa6347..1ad8bcf89 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst @@ -156,7 +156,8 @@ fn gather fold_pts_to arr #(p0 +. p1) s0 } -fn split (#t: Type) (s: ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t { SZ.v i <= Seq.length v }) +fn split (#t: Type) (s: ptr t) (#p: perm) (i: SZ.t) + (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v }) requires pts_to s #p v returns s' : ptr t ensures @@ -184,6 +185,36 @@ fn split (#t: Type) (s: ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ. s' } +ghost fn ghost_split (#t: Type) (s: ptr t) (#p: perm) (i: SZ.t) + (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v }) + requires pts_to s #p v + returns s' : erased (ptr t) + ensures + pts_to s #p (Seq.slice v 0 (SZ.v i)) ** + pts_to (reveal s') #p (Seq.slice v (SZ.v i) (Seq.length v)) ** + pure (adjacent s (SZ.v i) s') +{ + unfold_pts_to s #p v; + A.pts_to_range_prop s.base; + let s' = { + base = s.base; + offset = SZ.add s.offset i; + }; + A.pts_to_range_split s.base _ (SZ.v s'.offset) _; + with s1. assert A.pts_to_range s.base (SZ.v s.offset) (SZ.v s'.offset) #p s1; + rewrite + (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s'.offset) #p s1) + as (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + SZ.v i) #p s1); + fold_pts_to s #p s1; + with s2. assert A.pts_to_range s.base (SZ.v s'.offset) (SZ.v s.offset + Seq.length v) #p s2; + rewrite + (A.pts_to_range s.base (SZ.v s'.offset) (SZ.v s.offset + Seq.length v) #p s2) + as (A.pts_to_range s'.base (SZ.v s'.offset) (SZ.v s'.offset + Seq.length s2) #p s2); + fold_pts_to s' #p s2; + s' +} + + ghost fn join (#t: Type) (s1: ptr t) (#p: perm) (#v1: Seq.seq t) (s2: ptr t) (#v2: Seq.seq t) requires pts_to s1 #p v1 ** pts_to s2 #p v2 ** pure (adjacent s1 (Seq.length v1) s2) diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti index 3e308be45..7a911a975 100644 --- a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti +++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti @@ -106,7 +106,9 @@ val gather let adjacent #t (a: ptr t) (sz: nat) (b: ptr t) : prop = base a == base b /\ offset a + sz == offset b -val split (#t: Type) (s: ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t { SZ.v i <= Seq.length v }) : stt (ptr t) +val split (#t: Type) (s: ptr t) (#p: perm) (i: SZ.t) + (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v }) + : stt (ptr t) (requires pts_to s #p v) (ensures fun s' -> pts_to s #p (Seq.slice v 0 (SZ.v i)) ** @@ -114,6 +116,16 @@ val split (#t: Type) (s: ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ pure (adjacent s (SZ.v i) s') ) +val ghost_split (#t: Type) (s: ptr t) (#p: perm) (i: SZ.t) + (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v }) + : stt_ghost (erased (ptr t)) [] + (requires pts_to s #p v) + (ensures fun s' -> + pts_to s #p (Seq.slice v 0 (SZ.v i)) ** + pts_to (reveal s') #p (Seq.slice v (SZ.v i) (Seq.length v)) ** + pure (adjacent s (SZ.v i) s') + ) + val join (#t: Type) (s1: ptr t) (#p: perm) (#v1: Seq.seq t) (s2: ptr t) (#v2: Seq.seq t) : stt_ghost unit emp_inames (pts_to s1 #p v1 ** pts_to s2 #p v2 ** pure (adjacent s1 (Seq.length v1) s2)) (fun _ -> pts_to s1 #p (Seq.append v1 v2)) diff --git a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst index 809a8cfc8..789f9bc9b 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst @@ -97,3 +97,56 @@ fn split_trade (#t: Type) (s: S.slice t) (#p: perm) (i: SZ.t) (#v: Ghost.erased intro_trade _ _ _ (split_trade_aux s p v i s1 s2 v1 v2 ()); S.SlicePair s1 s2 } + +// TODO(GE): fix extraction for inline ghost functions (currently extracts to Obj.magic (fun _ -> ())) +ghost fn subslice_trade_mut_aux #t (s: slice t) (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v }) (res: slice t) (v': Seq.seq t) () + requires subslice_rest res s 1.0R i j v ** pts_to res v' + ensures pts_to s (Seq.slice v 0 (SZ.v i) `Seq.append` v' `Seq.append` Seq.slice v (SZ.v j) (Seq.length v)) +{ + unfold subslice_rest; + join res _ _; + join _ _ s; + assert pure ( + Seq.Base.append (Seq.Base.append (Seq.Base.slice v 0 (SZ.v i)) v') + (Seq.Base.slice v (SZ.v j) (Seq.Base.length v)) + `Seq.equal` + Seq.Base.append (Seq.Base.slice v 0 (SZ.v i)) + (Seq.Base.append v' (Seq.Base.slice v (SZ.v j) (Seq.Base.length v)))); +} + +inline_for_extraction +noextract +fn subslice_trade_mut #t (s: slice t) (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v }) + requires pts_to s v + returns res: slice t + ensures pts_to res (Seq.slice v (SZ.v i) (SZ.v j)) ** + (forall* v'. trade (pts_to res v') (pts_to s (Seq.slice v 0 (SZ.v i) `Seq.append` v' `Seq.append` Seq.slice v (SZ.v j) (Seq.length v)))) +{ + let res = subslice s i j; + intro_forall _ (fun v' -> intro_trade _ _ _ (subslice_trade_mut_aux s i j #v res v')); + res +} + +ghost fn subslice_trade_aux #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v }) (res: slice t) () + requires subslice_rest res s p i j v ** pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j)) + ensures pts_to s #p v +{ + unfold subslice_rest; + join res _ _; + join _ _ s; + assert pure (v `Seq.equal` Seq.append (Seq.slice v 0 (SZ.v i)) + (Seq.append (Seq.slice v (SZ.v i) (SZ.v j)) (Seq.slice v (SZ.v j) (Seq.length v)))); +} + +inline_for_extraction +noextract +fn subslice_trade #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v }) + requires pts_to s #p v + returns res: slice t + ensures pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j)) ** + trade (pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j))) (pts_to s #p v) +{ + let res = subslice s i j; + intro_trade _ _ _ (subslice_trade_aux s i j #v res); + res +} diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst index 85486df77..aa6f27ca0 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fst +++ b/lib/pulse/lib/Pulse.Lib.Slice.fst @@ -184,7 +184,7 @@ fn split (#t: Type) (s: slice t) (#p: perm) (i: SZ.t) { unfold_pts_to s #p v; Seq.lemma_split v (SZ.v i); - let elt' = AP.split s.elt #p #v i; + let elt' = AP.split s.elt #p i; let s1 = { elt = s.elt; len = i; @@ -211,6 +211,27 @@ fn join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: fold_pts_to s #p (Seq.append v1 v2) } +fn subslice #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v }) + requires pts_to s #p v + returns res: slice t + ensures pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j)) ** subslice_rest res s p i j v +{ + unfold_pts_to s #p v; + let elt' = AP.split s.elt i; + let elt'' = AP.ghost_split elt' (SZ.sub j i); + let s1 = hide { elt = s.elt; len = i }; + let s2 = hide { elt = elt'; len = SZ.sub s.len i }; + fold is_split s s1 s2; + let res = hide { elt = elt'; len = SZ.sub j i }; + let s3 = hide { elt = elt''; len = SZ.sub s.len j }; + fold is_split s2 res s3; + fold_pts_to s1 #p (Seq.slice v 0 (SZ.v i)); + fold_pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j)); + fold_pts_to s3 #p (Seq.slice v (SZ.v j) (Seq.length v)); + fold subslice_rest; + ({ elt = elt'; len = SZ.sub j i }) +} + fn copy (#t: Type) (dst: slice t) (#p: perm) (src: slice t) (#v: Ghost.erased (Seq.seq t)) requires diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Slice.fsti index b7fc4794b..20b8fe2a8 100644 --- a/lib/pulse/lib/Pulse.Lib.Slice.fsti +++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti @@ -17,6 +17,7 @@ module Pulse.Lib.Slice open FStar.Tactics.V2 open Pulse.Lib.Pervasives +open Pulse.Lib.Trade module SZ = FStar.SizeT module A = Pulse.Lib.Array @@ -110,6 +111,18 @@ val join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2 (pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s s1 s2) (fun _ -> pts_to s #p (Seq.append v1 v2)) +(* `subslice_rest r s p i j v` is the resource remaining after taking the subslice `r = s[i..j]` *) +let subslice_rest #t (r: slice t) (s: slice t) p (i j: SZ.t) (v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v }) : slprop = + exists* s1 s2 s3. + is_split s s1 s2 ** + is_split s2 r s3 ** + pts_to s1 #p (Seq.slice v 0 (SZ.v i)) ** + pts_to s3 #p (Seq.slice v (SZ.v j) (Seq.length v)) + +val subslice #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v }) : + stt (slice t) (pts_to s #p v) + fun res -> pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j)) ** subslice_rest res s p i j v + val copy (#t: Type) (dst: slice t) (#p: perm) (src: slice t) (#v: Ghost.erased (Seq.seq t)) : stt unit (exists* v_dst . pts_to dst v_dst ** pts_to src #p v ** pure (len src == len dst)) (fun _ -> pts_to dst v ** pts_to src #p v) diff --git a/pulse2rust/src/Pulse2Rust.Extract.fst b/pulse2rust/src/Pulse2Rust.Extract.fst index 544078d48..b4ae444b0 100644 --- a/pulse2rust/src/Pulse2Rust.Extract.fst +++ b/pulse2rust/src/Pulse2Rust.Extract.fst @@ -660,6 +660,10 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr = | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e::_::i::_) when S.string_of_mlpath p = "Pulse.Lib.Slice.split" -> mk_method_call (extract_mlexpr g e) "split_at_mut" [extract_mlexpr g i] + | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, s::_::a::b::_) + when S.string_of_mlpath p = "Pulse.Lib.Slice.subslice" -> + let mutb = true in + mk_reference_expr true (mk_expr_index (extract_mlexpr g s) (mk_range (Some (extract_mlexpr g a)) RangeLimitsHalfOpen (Some (extract_mlexpr g b)))) | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, a::_::b::_) when S.string_of_mlpath p = "Pulse.Lib.Slice.copy" -> mk_method_call (extract_mlexpr g a) "copy_from_slice" [extract_mlexpr g b] diff --git a/pulse2rust/src/Pulse2Rust.Rust.Syntax.fst b/pulse2rust/src/Pulse2Rust.Rust.Syntax.fst index ce46a886d..1f774e1f2 100644 --- a/pulse2rust/src/Pulse2Rust.Rust.Syntax.fst +++ b/pulse2rust/src/Pulse2Rust.Rust.Syntax.fst @@ -189,6 +189,13 @@ let mk_cast (e:expr) (ty:typ) : expr = expr_cast_type = ty; } +let mk_range (s:option expr) (l:range_limits) (e:option expr) : expr = + Expr_range { + expr_range_start = s; + expr_range_limits = l; + expr_range_end = e; + } + let mk_new_mutex (e:expr) = mk_call (mk_expr_path ["std"; "sync"; "Mutex"; "new"]) diff --git a/pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti b/pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti index 51ab5ddd8..3365fb17a 100644 --- a/pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti +++ b/pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti @@ -112,6 +112,7 @@ and expr = | Expr_tuple of list expr | Expr_method_call of expr_method_call | Expr_cast of expr_cast + | Expr_range of expr_range and expr_bin = { expr_bin_left : expr; @@ -197,6 +198,16 @@ and expr_cast = { expr_cast_type : typ; } +and expr_range = { + expr_range_start: option expr; + expr_range_limits: range_limits; + expr_range_end: option expr; +} + +and range_limits = + | RangeLimitsHalfOpen + | RangeLimitsClosed + and local_stmt = { local_stmt_pat : option pat; local_stmt_init : option expr; @@ -358,6 +369,7 @@ val mk_expr_tuple (l:list 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_cast (e:expr) (ty:typ) : expr +val mk_range (s:option expr) (l:range_limits) (e:option expr) : expr val mk_new_mutex (e:expr) : expr val mk_lock_mutex (e:expr) : expr diff --git a/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml b/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml index 27129e1d3..b0332d8ee 100644 --- a/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml +++ b/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml @@ -1240,6 +1240,36 @@ and (extract_mlexpr : let uu___7 = extract_mlexpr g e1 in let uu___8 = let uu___9 = extract_mlexpr g i in [uu___9] in Pulse2Rust_Rust_Syntax.mk_method_call uu___7 "split_at_mut" uu___8 + | FStarC_Extraction_ML_Syntax.MLE_App + ({ + FStarC_Extraction_ML_Syntax.expr = + FStarC_Extraction_ML_Syntax.MLE_TApp + ({ + FStarC_Extraction_ML_Syntax.expr = + FStarC_Extraction_ML_Syntax.MLE_Name p; + FStarC_Extraction_ML_Syntax.mlty = uu___; + FStarC_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2::[]); + FStarC_Extraction_ML_Syntax.mlty = uu___3; + FStarC_Extraction_ML_Syntax.loc = uu___4;_}, + s::uu___5::a::b::uu___6) + when + let uu___7 = FStarC_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Pulse.Lib.Slice.subslice" -> + let mutb = true in + let uu___7 = + let uu___8 = extract_mlexpr g s in + let uu___9 = + let uu___10 = + let uu___11 = extract_mlexpr g a in + FStar_Pervasives_Native.Some uu___11 in + let uu___11 = + let uu___12 = extract_mlexpr g b in + FStar_Pervasives_Native.Some uu___12 in + Pulse2Rust_Rust_Syntax.mk_range uu___10 + Pulse2Rust_Rust_Syntax.RangeLimitsHalfOpen uu___11 in + Pulse2Rust_Rust_Syntax.mk_expr_index uu___8 uu___9 in + Pulse2Rust_Rust_Syntax.mk_reference_expr true uu___7 | FStarC_Extraction_ML_Syntax.MLE_App ({ FStarC_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 239ac33d2..35127ce42 100644 --- a/pulse2rust/src/ocaml/generated/Pulse2Rust_Rust_Syntax.ml +++ b/pulse2rust/src/ocaml/generated/Pulse2Rust_Rust_Syntax.ml @@ -163,6 +163,7 @@ and expr = | Expr_tuple of expr Prims.list | Expr_method_call of expr_method_call | Expr_cast of expr_cast + | Expr_range of expr_range and expr_bin = { expr_bin_left: expr ; @@ -221,6 +222,14 @@ and expr_method_call = and expr_cast = { expr_cast_expr: expr ; expr_cast_type: typ } +and expr_range = + { + expr_range_start: expr FStar_Pervasives_Native.option ; + expr_range_limits: range_limits ; + expr_range_end: expr FStar_Pervasives_Native.option } +and range_limits = + | RangeLimitsHalfOpen + | RangeLimitsClosed and local_stmt = { local_stmt_pat: pat FStar_Pervasives_Native.option ; @@ -406,6 +415,11 @@ let (uu___is_Expr_cast : expr -> Prims.bool) = match projectee with | Expr_cast _0 -> true | uu___ -> false let (__proj__Expr_cast__item___0 : expr -> expr_cast) = fun projectee -> match projectee with | Expr_cast _0 -> _0 +let (uu___is_Expr_range : expr -> Prims.bool) = + fun projectee -> + match projectee with | Expr_range _0 -> true | uu___ -> false +let (__proj__Expr_range__item___0 : expr -> expr_range) = + fun projectee -> match projectee with | Expr_range _0 -> _0 let (__proj__Mkexpr_bin__item__expr_bin_left : expr_bin -> expr) = fun projectee -> match projectee with @@ -567,6 +581,30 @@ let (__proj__Mkexpr_cast__item__expr_cast_type : expr_cast -> typ) = fun projectee -> match projectee with | { expr_cast_expr; expr_cast_type;_} -> expr_cast_type +let (__proj__Mkexpr_range__item__expr_range_start : + expr_range -> expr FStar_Pervasives_Native.option) = + fun projectee -> + match projectee with + | { expr_range_start; expr_range_limits; expr_range_end;_} -> + expr_range_start +let (__proj__Mkexpr_range__item__expr_range_limits : + expr_range -> range_limits) = + fun projectee -> + match projectee with + | { expr_range_start; expr_range_limits; expr_range_end;_} -> + expr_range_limits +let (__proj__Mkexpr_range__item__expr_range_end : + expr_range -> expr FStar_Pervasives_Native.option) = + fun projectee -> + match projectee with + | { expr_range_start; expr_range_limits; expr_range_end;_} -> + expr_range_end +let (uu___is_RangeLimitsHalfOpen : range_limits -> Prims.bool) = + fun projectee -> + match projectee with | RangeLimitsHalfOpen -> true | uu___ -> false +let (uu___is_RangeLimitsClosed : range_limits -> Prims.bool) = + fun projectee -> + match projectee with | RangeLimitsClosed -> true | uu___ -> false let (__proj__Mklocal_stmt__item__local_stmt_pat : local_stmt -> pat FStar_Pervasives_Native.option) = fun projectee -> @@ -1088,6 +1126,15 @@ let (mk_method_call : expr -> Prims.string -> expr Prims.list -> expr) = } let (mk_cast : expr -> typ -> expr) = fun e -> fun ty -> Expr_cast { expr_cast_expr = e; expr_cast_type = ty } +let (mk_range : + expr FStar_Pervasives_Native.option -> + range_limits -> expr FStar_Pervasives_Native.option -> expr) + = + fun s -> + fun l -> + fun e -> + Expr_range + { expr_range_start = s; expr_range_limits = l; expr_range_end = e } let (mk_new_mutex : expr -> expr) = fun e -> let uu___ = mk_expr_path ["std"; "sync"; "Mutex"; "new"] in diff --git a/pulse2rust/src/ocaml/rust/src/lib.rs b/pulse2rust/src/ocaml/rust/src/lib.rs index f53b58a2b..6a1dfcf25 100644 --- a/pulse2rust/src/ocaml/rust/src/lib.rs +++ b/pulse2rust/src/ocaml/rust/src/lib.rs @@ -142,6 +142,17 @@ struct ExprCast { expr_cast_type: Box, } +struct ExprRange { + expr_range_start: Option>, + expr_range_limits: RangeLimits, + expr_range_end: Option>, +} + +enum RangeLimits { + RangeLimitsHalfOpen, + RangeLimitsClosed, +} + enum Expr { EBinOp(ExprBin), EPath(Vec), @@ -161,6 +172,7 @@ enum Expr { ETuple(Vec), EMethodCall(ExprMethodCall), ECast(ExprCast), + ERange(ExprRange), } struct TypeReference { @@ -401,6 +413,7 @@ impl_from_ocaml_variant! { Expr::ETuple (payload:OCamlList), Expr::EMethodCall (payload:ExprMethodCall), Expr::ECast (payload:ExprCast), + Expr::ERange (payload:ExprRange) } } @@ -520,6 +533,21 @@ impl_from_ocaml_record! { } } +impl_from_ocaml_record! { + ExprRange { + expr_range_start: Option, + expr_range_limits: RangeLimits, + expr_range_end: Option, + } +} + +impl_from_ocaml_variant! { + RangeLimits { + RangeLimits::RangeLimitsHalfOpen, + RangeLimits::RangeLimitsClosed, + } +} + impl_from_ocaml_record! { TypeReference { type_reference_mut: bool, @@ -1203,6 +1231,17 @@ fn to_syn_expr(e: &Expr) -> syn::Expr { ty: Box::new(to_syn_typ(expr_cast_type)), }) }, + Expr::ERange(ExprRange { expr_range_start, expr_range_limits, expr_range_end }) => { + syn::Expr::Range(syn::ExprRange { + attrs: vec![], + start: expr_range_start.as_ref().map(|e| Box::new(to_syn_expr(e))), + limits: (match expr_range_limits { + RangeLimits::RangeLimitsHalfOpen => syn::RangeLimits::HalfOpen(syn::token::DotDot { spans: [Span::call_site(), Span::call_site()] }), + RangeLimits::RangeLimitsClosed => syn::RangeLimits::Closed(syn::token::DotDotEq { spans: [Span::call_site(), Span::call_site(), Span::call_site()] }), + }), + end: expr_range_end.as_ref().map(|e| Box::new(to_syn_expr(e))), + }) + }, } } @@ -2142,6 +2181,15 @@ impl fmt::Display for Expr { expr_cast_expr, expr_cast_type, ), + Expr::ERange(ExprRange { expr_range_start, expr_range_limits, expr_range_end }) => { + if let Some(e) = expr_range_start { write!(f, "{}", e)? } + write!(f, " {} ", match expr_range_limits { + RangeLimits::RangeLimitsHalfOpen => "..", + RangeLimits::RangeLimitsClosed => "..=", + })?; + if let Some(e) = expr_range_end { write!(f, "{}", e)? } + Ok(()) + }, } } } diff --git a/pulse2rust/tests/src/example_slice.rs b/pulse2rust/tests/src/example_slice.rs index 17fde9346..26a573e94 100644 --- a/pulse2rust/tests/src/example_slice.rs +++ b/pulse2rust/tests/src/example_slice.rs @@ -9,7 +9,11 @@ pub fn test(arr: &mut [u8]) -> () { let _letpattern = slice.split_at_mut(2); match _letpattern { (mut s1, mut s2) => { - let x = s2[s1.len()]; + let s2_ = { + let res = &mut s2[1..4]; + res + }; + let x = s2_[s1.len()]; s1[1] = x; let _letpattern1 = s2.split_at_mut(2); match _letpattern1 { diff --git a/share/pulse/examples/Example.Slice.fst b/share/pulse/examples/Example.Slice.fst index ded284bfe..d55d47f1e 100644 --- a/share/pulse/examples/Example.Slice.fst +++ b/share/pulse/examples/Example.Slice.fst @@ -16,19 +16,22 @@ module Example.Slice #lang-pulse open Pulse -open Pulse.Lib.Slice +open Pulse.Lib.Trade +open Pulse.Lib.Slice.Util module A = Pulse.Lib.Array fn test (arr: A.array UInt8.t) requires pts_to arr seq![0uy; 1uy; 2uy; 3uy; 4uy; 5uy] - ensures exists* s. pts_to arr s ** pure (s `Seq.equal` seq![0uy; 4uy; 4uy; 5uy; 4uy; 5uy]) { + ensures exists* s. pts_to arr s ** pure (s `Seq.equal` seq![0uy; 5uy; 4uy; 5uy; 4uy; 5uy]) { A.pts_to_len arr; let slice = from_array arr 6sz; let SlicePair s1 s2 = split slice 2sz; pts_to_len s1; share s2; - let x = s2.(len s1); + let s2' = subslice_trade s2 1sz 4sz; + let x = s2'.(len s1); s1.(1sz) <- x; + elim_trade _ _; gather s2; let SlicePair s3 s4 = split s2 2sz; pts_to_len s3; diff --git a/src/extraction/ExtractPulse.fst b/src/extraction/ExtractPulse.fst index 1dea57c52..ba6c820c7 100644 --- a/src/extraction/ExtractPulse.fst +++ b/src/extraction/ExtractPulse.fst @@ -128,7 +128,7 @@ let pulse_translate_expr : translate_expr_t = fun env e -> when string_of_mlpath p = "Pulse.Lib.ArrayPtr.from_array" -> translate_expr env x - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ a; _p; _w; i ]) + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ a; _p; i; _w ]) when string_of_mlpath p = "Pulse.Lib.ArrayPtr.split" -> EBufSub (translate_expr env a, translate_expr env i) diff --git a/src/ocaml/plugin/generated/ExtractPulse.ml b/src/ocaml/plugin/generated/ExtractPulse.ml index 08713b018..6b92a1c9e 100644 --- a/src/ocaml/plugin/generated/ExtractPulse.ml +++ b/src/ocaml/plugin/generated/ExtractPulse.ml @@ -455,7 +455,7 @@ let (pulse_translate_expr : FStarC_Extraction_Krml.translate_expr_t) = uu___3); FStarC_Extraction_ML_Syntax.mlty = uu___4; FStarC_Extraction_ML_Syntax.loc = uu___5;_}, - a::_p::_w::i::[]) + a::_p::i::_w::[]) when let uu___6 = FStarC_Extraction_ML_Syntax.string_of_mlpath p in uu___6 = "Pulse.Lib.ArrayPtr.split" ->