Merge #132

132: Add array update r=W95Psp a=franziskuskiefer

This is not complete but is a step in the right direction.

Co-authored-by: Karthikeyan Bhargavan <[email protected]>
Co-authored-by: Franziskus Kiefer <[email protected]>
Co-authored-by: Lucas Franceschino <[email protected]>

engine/backends/coq/coq/coq_backend.ml

@@ -306,7 +306,12 @@ struct
 
   (* let is_field_an_index = index_of_field >> Option.is_some *)
 
-  let rec pexpr (e : expr) : C.AST.term =
+  let rec pexpr (e : expr) =
+    try pexpr_unwrapped e
+    with Diagnostics.SpanFreeError kind ->
+      TODOs_debug.__TODO_term__ e.span "failure"
+
+  and pexpr_unwrapped (e : expr) : C.AST.term =
     let span = e.span in
     match e.e with
     | Literal e -> C.AST.Const (pliteral e)
@@ -386,6 +391,11 @@ struct
     | _ -> .
 
   let rec pitem (e : item) : C.AST.decl list =
+    try pitem_unwrapped e
+    with Diagnostics.SpanFreeError _kind ->
+      [ C.AST.Unimplemented "item error backend" ]
+
+  and pitem_unwrapped (e : item) : C.AST.decl list =
     let span = e.span in
     match e.v with
     | Fn { name; generics; body; params } ->

engine/backends/fstar/fstar_backend.ml

@@ -214,6 +214,22 @@ struct
     >> map_last_global_ident (fun s -> s ^ "_t")
     >> pglobal_ident span
 
+  (* This is a bit too fiddly. TODO: simplify *)
+  let pfield_concrete_ident (id : concrete_ident) =
+    let id_path = Non_empty_list.to_list id.path in
+    F.lid [ String.lowercase (List.last_exn id_path) ]
+
+  let pfield_ident span (f : global_ident) : F.Ident.lident =
+    match f with
+    | `Concrete cid -> pfield_concrete_ident cid
+    | `Projector (`TupleField (n, len)) | `TupleField (n, len) ->
+        F.lid [ "_" ^ Int.to_string (n + 1) ]
+    | `Projector (`Concrete cid) -> pfield_concrete_ident cid
+    | _ ->
+        Error.assertion_failure span
+          ("pfield_ident: not a valid field name in F* backend: "
+         ^ show_global_ident f)
+
   let pconstructor_ident span : global_ident -> F.Ident.lident =
     uppercase_global_ident >> pglobal_ident span
 
@@ -298,8 +314,8 @@ struct
                 (F.term_of_lid [ "FStar"; "List"; "Tot"; "Base"; "length" ])
                 [ x ]
             in
-            let lt = F.term @@ F.AST.Name (pprim_ident span @@ BinOp Lt) in
-            F.mk_e_app lt [ len_of_x; pexpr length ])
+            let eq = F.term @@ F.AST.Name (pprim_ident span @@ BinOp Eq) in
+            F.mk_e_app eq [ len_of_x; pexpr length ])
     | TParam i ->
         F.term
         @@ F.AST.Var
@@ -388,7 +404,7 @@ struct
         @@ F.AST.Project (pexpr arg, F.lid [ "_" ^ string_of_int (n + 1) ])
     | App { f = { e = GlobalVar (`Projector (`Concrete cid)) }; args = [ arg ] }
       ->
-        F.term @@ F.AST.Project (pexpr arg, pconcrete_ident cid)
+        F.term @@ F.AST.Project (pexpr arg, pfield_concrete_ident cid)
     | App { f = { e = GlobalVar x }; args } when Map.mem operators x ->
         let arity, op = Map.find_exn operators x in
         if List.length args <> arity then
@@ -436,7 +452,7 @@ struct
         @@ F.AST.Record
              ( Option.map ~f:(fst >> pexpr) base,
                List.map
-                 ~f:(fun (f, e) -> (pglobal_ident e.span f, pexpr e))
+                 ~f:(fun (f, e) -> (pfield_ident e.span f, pexpr e))
                  fields )
     | Construct { constructs_record = false; constructor; fields; base }
       when List.for_all ~f:(fst >> is_field_an_index) fields ->

engine/lib/import_thir.ml

@@ -252,6 +252,22 @@ module Exn = struct
           args = [ { e = Borrow { e = x; _ }; _ }; index ];
         } ->
         Some (x, index)
+    | App
+        {
+          f =
+            {
+              e =
+                GlobalVar
+                  (`Concrete
+                    {
+                      crate = "core";
+                      path = Non_empty_list.[ "ops"; "Index"; "index" ];
+                    });
+              _;
+            };
+          args = [ x; index ];
+        } ->
+        Some (x, index)
     | _ -> None
 
   let rec c_expr (e : Thir.decorated_for__expr_kind) : expr =
@@ -545,7 +561,7 @@ module Exn = struct
             (mk_global ([ lhs_type; index_type ] ->. typ)
             @@ `Concrete
                  {
-                   crate = "std";
+                   crate = "core";
                    path = Non_empty_list.[ "ops"; "Index"; "index" ];
                  })
             [ lhs; index ]
@@ -581,7 +597,7 @@ module Exn = struct
                   {
                     f =
                       {
-                        e = GlobalVar (`Projector (`Concrete _) as field);
+                        e = GlobalVar (`Projector _ as field);
                         typ = TArrow ([ _ ], _);
                         span = _;
                       };

engine/lib/phases/phase_trivialize_assign_lhs.ml

@@ -8,6 +8,7 @@ module%inlined_contents Make (F : Features.T) = struct
   module FB = struct
     include F
     include Features.Off.Nontrivial_lhs
+    include Features.On.Construct_base
   end
 
   include
@@ -21,6 +22,8 @@ module%inlined_contents Make (F : Features.T) = struct
 
     module S = struct
       include Features.SUBTYPE.Id
+
+      let construct_base _ = Features.On.construct_base
     end
 
     module UA = Ast_utils.Make (F)
@@ -60,9 +63,27 @@ module%inlined_contents Make (F : Features.T) = struct
         (LocalIdent.t * B.ty) * B.expr =
       match lhs with
       | LhsLocalVar { var; typ } -> ((var, dty span typ), rhs)
-      | LhsFieldAccessor _ ->
-          Error.unimplemented ~issue_id:86
-            ~details:"Mutation of fields is not implemented yet" span
+      | LhsFieldAccessor { e; typ; field; _ } -> (
+          let lhs = expr_of_lhs e span in
+          let field =
+            match field with
+            | `Projector field -> (field :> global_ident)
+            | _ -> field
+          in
+          match lhs.typ with
+          | TApp { ident; args } ->
+              let rhs' =
+                B.Construct
+                  {
+                    constructor = ident;
+                    constructs_record = true;
+                    fields = [ (field, rhs) ];
+                    base = Some (lhs, Features.On.construct_base);
+                  }
+              in
+              let rhs = { B.e = rhs'; typ = lhs.typ; span } in
+              updater_of_lhs e rhs span
+          | _ -> Error.raise { kind = ArbitraryLHS; span })
       | LhsArrayAccessor { e; typ = _; index; _ } ->
           let lhs = expr_of_lhs e span in
           let rhs =

engine/lib/phases/phase_trivialize_assign_lhs.mli

@@ -9,6 +9,7 @@ module Make (F : Features.T) : sig
     module FB = struct
       include F
       include Features.Off.Nontrivial_lhs
+      include Features.On.Construct_base
     end
 
     module A = Ast.Make (F)

tests/side-effects/Cargo.toml

@@ -7,4 +7,4 @@ edition = "2021"
 
 [package.metadata.hax-tests]
 into.fstar = {snapshot = "none"}
-into.coq = {snapshot = "none"}
+into.coq = {broken = true, snapshot = "none", issue_id = 134}

tests/side-effects/src/lib.rs

@@ -1,8 +1,8 @@
+#![allow(dead_code)]
 fn add3(x: usize, y: usize, z: usize) -> usize {
     x + y + z
 }
 
-#[allow(dead_code)]
 fn local_mutation(mut x: usize) -> usize {
     let mut y = 0;
     if {
@@ -39,7 +39,6 @@ fn local_mutation(mut x: usize) -> usize {
     }
 }
 
-#[allow(dead_code)]
 fn early_returns(mut x: usize) -> usize {
     return (123
         + if {
@@ -59,7 +58,6 @@ fn early_returns(mut x: usize) -> usize {
         + x;
 }
 
-#[allow(dead_code)]
 fn question_mark(mut x: usize) -> Result<usize, usize> {
     if x > 40usize {
         let mut y = 0;
@@ -78,3 +76,22 @@ fn question_mark(mut x: usize) -> Result<usize, usize> {
     };
     Ok(3 + x)
 }
+
+struct Bar {
+    a: bool,
+    b: ([(bool, bool); 6], bool),
+}
+struct Foo {
+    x: bool,
+    y: (bool, Vec<Bar>),
+    z: [Bar; 6],
+    bar: Bar,
+}
+fn assign_non_trivial_lhs(mut foo: Foo) -> Foo {
+    foo.x = true;
+    foo.bar.a = true;
+    foo.bar.b.0[3].1 = true;
+    foo.z[3].a = true;
+    foo.y.1[3].b.0[5].0 = true;
+    foo
+}