pulse2rust: Slice.len

FStarLang · Oct 8, 2024 · 24f4886 · 24f4886
1 parent 56cfbb9
commit 24f4886
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 2 deletions.
diff --git a/pulse2rust/src/Pulse2Rust.Extract.fst b/pulse2rust/src/Pulse2Rust.Extract.fst
@@ -663,6 +663,9 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr =
   | 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]
+  | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, [a])
+    when S.string_of_mlpath p = "Pulse.Lib.Slice.len" ->
+    mk_method_call (extract_mlexpr g a) "len" []
 
     //
     // vec_as_array e extracted to &mut e

diff --git a/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml b/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml
@@ -1256,6 +1256,24 @@ and (extract_mlexpr :
           let uu___8 = let uu___9 = extract_mlexpr g b in [uu___9] in
           Pulse2Rust_Rust_Syntax.mk_method_call uu___7 "copy_from_slice"
             uu___8
+      | 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;_},
+           a::[])
+          when
+          let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+          uu___5 = "Pulse.Lib.Slice.len" ->
+          let uu___5 = extract_mlexpr g a in
+          Pulse2Rust_Rust_Syntax.mk_method_call uu___5 "len" []
       | FStar_Extraction_ML_Syntax.MLE_App
           ({
              FStar_Extraction_ML_Syntax.expr =

diff --git a/pulse2rust/tests/src/example_slice.rs b/pulse2rust/tests/src/example_slice.rs
@@ -9,7 +9,7 @@ pub fn test(arr: &mut [u8]) -> () {
     let _letpattern = slice.split_at_mut(2);
     match _letpattern {
         (mut s1, mut s2) => {
-            let x = s2[2];
+            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
@@ -25,8 +25,9 @@ fn test (arr: A.array UInt8.t)
   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.(2sz);
+  let x = s2.(len s1);
   s1.(1sz) <- x;
   gather s2;
   let SlicePair s3 s4 = split s2 2sz;